Commit 88cf739f authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Bring up the boolean type. 

Add the necessary pieces to the boolean type, so that the CVC3 code can
generate for it.  Currently the only failing issue is some operators to actually
make use of it.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10467 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 7df7d7a4

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/BooleanVariableType.java

+11 −0
Original line number Diff line number Diff line
@@ -9,6 +9,17 @@ package ca.mcmaster.cas.matlab2smt; 
 * @author matthew

 */

public class BooleanVariableType implements VariableType {



    @Override

    public boolean equals(Object other) {

        return other instanceof BooleanVariableType;

    }



    @Override

    public int hashCode() {

        return 0;

    }



    @Override

    public boolean canCastToType(VariableType type) {

        return false;

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/VariableParser.g4

+3 −1
Original line number Diff line number Diff line
@@ -5,10 +5,12 @@ var: ID vartype; 
vartype: ':' type_info

       | defaulttype;

defaulttype: ;

type_info: 'bool'

type_info: bool_type

         | real_type

         | fixed_type ;



bool_type: 'bool';



real_type: 'real';



fixed_type: 'fixedt(' NAT ',' NAT ')'

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/VariableParser.java

+6 −0
Original line number Diff line number Diff line
@@ -4,6 +4,7 @@ 
 */

package ca.mcmaster.cas.matlab2smt;



import ca.mcmaster.cas.matlab2smt.VariableParserParser.Bool_typeContext;

import ca.mcmaster.cas.matlab2smt.VariableParserParser.DefaulttypeContext;

import ca.mcmaster.cas.matlab2smt.VariableParserParser.Fixed_typeContext;

import ca.mcmaster.cas.matlab2smt.VariableParserParser.Real_typeContext;
@@ -92,6 +93,11 @@ public class VariableParser { 
            currentType = new RealVariableType();

        }



        @Override

        public void enterBool_type(Bool_typeContext ctx) {

            currentType = new BooleanVariableType();

        }



        @Override

        public void enterFixed_type(Fixed_typeContext ctx) {

            boolean signed = (ctx.NAT(0).getText().equals("0"))?false:true;

Matlab2SMT/src/test/java/ca/mcmaster/cas/matlab2smt/test/BooleanVariableTypeTest.java

0 → 100644
+71 −0
Original line number Diff line number Diff line 
/*

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcmaster.cas.matlab2smt.test;



import ca.mcmaster.cas.matlab2smt.BooleanVariableType;

import ca.mcmaster.cas.matlab2smt.CVC3Generator;

import ca.mcmaster.cas.matlab2smt.CheckerGenerator;

import ca.mcmaster.cas.matlab2smt.RealVariableType;

import org.junit.After;

import org.junit.AfterClass;

import org.junit.Before;

import org.junit.BeforeClass;

import org.junit.Test;

import static org.junit.Assert.*;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



/**

 *

 * @author matthew

 */

@RunWith(JUnit4.class)

public class BooleanVariableTypeTest {



    /**

     * Test of getCVC3Definition method, of class RealVariableType.

     */

    @Test

    public void testGetCVC3Definition() {

        String variableName = "test_variable";

        BooleanVariableType instance = new BooleanVariableType();

        String expResult = "BOOLEAN";

        String result = generator.GenerateVariableType(instance);

        assertEquals(expResult, result);

    }



    /**

     * Test of equals method, of class RealVariableType.

     */

    @Test

    public void testEquals() {

        BooleanVariableType test = new BooleanVariableType();

        assertTrue(test.equals(new BooleanVariableType()));

        assertTrue(test.equals(test));

        assertFalse(test.equals(new Object()));

    }



    /**

     * Test of hashCode method, of class RealVariableType.

     */

    @Test

    public void testHashCode() {

        BooleanVariableType instance = new BooleanVariableType();

        assertEquals(0, instance.hashCode());

    }



    /**

     * Test of canCastToType method, of class RealVariableType.  Reals (for now)

     * don't cast.

     */

    @Test

    public void testCanCastToType() {

        BooleanVariableType instance = new BooleanVariableType();

        assertFalse(instance.canCastToType(new RealVariableType()));

        assertFalse(instance.canCastToType(new BooleanVariableType()));

    }



    CheckerGenerator generator = new CVC3Generator();

}