From 0398c53a582a3242ef89dceae59d00137f17df79 Mon Sep 17 00:00:00 2001 From: makaimann Date: Tue, 18 Feb 2020 20:11:52 -0800 Subject: Change datatype selector/constructor/tester to terms (#3773) --- test/unit/api/solver_black.h | 93 ++++++++++++++++++++++++-------------------- test/unit/api/term_black.h | 92 ++++++++++++++++++++++++++++++++++++++----- 2 files changed, 133 insertions(+), 52 deletions(-) (limited to 'test/unit') diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 2831b840d..e53b989f0 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -642,47 +642,55 @@ void SolverBlack::testMkTermFromOp() Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Op consTerm1 = list.getConstructorTerm("cons"); - Op consTerm2 = list.getConstructor("cons").getConstructorTerm(); - Op nilTerm1 = list.getConstructorTerm("nil"); - Op nilTerm2 = list.getConstructor("nil").getConstructorTerm(); - Op headTerm1 = list["cons"].getSelectorTerm("head"); - Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); - Op tailTerm1 = list["cons"].getSelectorTerm("tail"); - Op tailTerm2 = list["cons"]["tail"].getSelectorTerm(); - - // mkTerm(Kind kind, Op op) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2)); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&); + Term consTerm1 = list.getConstructorTerm("cons"); + Term consTerm2 = list.getConstructor("cons").getConstructorTerm(); + Term nilTerm1 = list.getConstructorTerm("nil"); + Term nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + Term headTerm1 = list["cons"].getSelectorTerm("head"); + Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); + Term tailTerm1 = list["cons"].getSelectorTerm("tail"); + Term tailTerm2 = list["cons"]["tail"].getSelectorTerm(); + + // mkTerm(Op op, Term term) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, nilTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, consTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child) const + // mkTerm(Op op, Term child) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c)); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)), - CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), + CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child1, Term child2) const + // mkTerm(Op op, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1))); + TS_ASSERT_THROWS_NOTHING( + d_solver->mkTerm(APPLY_CONSTRUCTOR, + consTerm1, + d_solver->mkReal(0), + d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) + // mkTerm(Op op, Term child1, Term child2, Term child3) // const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); @@ -942,26 +950,23 @@ void SolverBlack::testGetOp() Sort consListSort = d_solver->mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Op consTerm = consList.getConstructorTerm("cons"); - Op nilTerm = consList.getConstructorTerm("nil"); - Op headTerm = consList["cons"].getSelectorTerm("head"); - - TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR); - TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR); - TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR); + Term consTerm = consList.getConstructorTerm("cons"); + Term nilTerm = consList.getConstructorTerm("nil"); + Term headTerm = consList["cons"].getSelectorTerm("head"); - Term listnil = d_solver->mkTerm(nilTerm); - Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil); - Term listhead = d_solver->mkTerm(headTerm, listcons1); + Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm); + Term listcons1 = d_solver->mkTerm( + APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil); + Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1); TS_ASSERT(listnil.hasOp()); - TS_ASSERT_EQUALS(listnil.getOp(), nilTerm); + TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR); TS_ASSERT(listcons1.hasOp()); - TS_ASSERT_EQUALS(listcons1.getOp(), consTerm); + TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR); TS_ASSERT(listhead.hasOp()); - TS_ASSERT_EQUALS(listhead.getOp(), headTerm); + TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR); } void SolverBlack::testPush1() @@ -1074,12 +1079,14 @@ void SolverBlack::testSimplify() TS_ASSERT(i1 == d_solver->simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = - d_solver->mkTerm(consList.getConstructorTerm("cons"), - d_solver->mkReal(0), - d_solver->mkTerm(consList.getConstructorTerm("nil"))); + Term dt1 = d_solver->mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + d_solver->mkReal(0), + d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1)); - Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1); + Term dt2 = d_solver->mkTerm( + APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2)); Term b1 = d_solver->mkVar(bvSort, "b1"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 0d5400f5f..ea619db7c 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -28,8 +28,8 @@ class TermBlack : public CxxTest::TestSuite void testGetId(); void testGetKind(); void testGetSort(); + void testGetOp(); void testIsNull(); - void testIsParameterized(); void testNotTerm(); void testAndTerm(); void testOrTerm(); @@ -152,6 +152,88 @@ void TermBlack::testGetSort() TS_ASSERT(p_f_y.getSort() == boolSort); } +void TermBlack::testGetOp() +{ + Sort intsort = d_solver.getIntegerSort(); + Sort bvsort = d_solver.mkBitVectorSort(8); + Sort arrsort = d_solver.mkArraySort(bvsort, intsort); + Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); + + Term x = d_solver.mkConst(intsort, "x"); + Term a = d_solver.mkConst(arrsort, "a"); + Term b = d_solver.mkConst(bvsort, "b"); + + TS_ASSERT(!x.hasOp()); + TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&); + + Term ab = d_solver.mkTerm(SELECT, a, b); + Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + Term extb = d_solver.mkTerm(ext, b); + + TS_ASSERT(ab.hasOp()); + TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT)); + TS_ASSERT(!ab.getOp().isIndexed()); + // can compare directly to a Kind (will invoke Op constructor) + TS_ASSERT_EQUALS(ab.getOp(), SELECT); + TS_ASSERT(extb.hasOp()); + TS_ASSERT(extb.getOp().isIndexed()); + TS_ASSERT_EQUALS(extb.getOp(), ext); + + Term f = d_solver.mkConst(funsort, "f"); + Term fx = d_solver.mkTerm(APPLY_UF, f, x); + + TS_ASSERT(!f.hasOp()); + TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&); + TS_ASSERT(fx.hasOp()); + TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF); + std::vector children(fx.begin(), fx.end()); + // testing rebuild from op and children + TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children)); + + // Test Datatypes Ops + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil("nil"); + DatatypeSelectorDecl head("head", sort); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + listDecl.addConstructor(cons); + listDecl.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(listDecl); + Sort intListSort = + listSort.instantiate(std::vector{d_solver.getIntegerSort()}); + Term c = d_solver.mkConst(intListSort, "c"); + Datatype list = listSort.getDatatype(); + // list datatype constructor and selector operator terms + Term consOpTerm = list.getConstructorTerm("cons"); + Term nilOpTerm = list.getConstructorTerm("nil"); + Term headOpTerm = list["cons"].getSelectorTerm("head"); + Term tailOpTerm = list["cons"].getSelectorTerm("tail"); + + Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); + Term consTerm = d_solver.mkTerm( + APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm); + Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); + Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); + + TS_ASSERT(nilTerm.hasOp()); + TS_ASSERT(consTerm.hasOp()); + TS_ASSERT(headTerm.hasOp()); + TS_ASSERT(tailTerm.hasOp()); + + TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR); + TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR); + + // Test rebuilding + children.clear(); + children.insert(children.begin(), headTerm.begin(), headTerm.end()); + TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); +} + void TermBlack::testIsNull() { Term x; @@ -189,14 +271,6 @@ void TermBlack::testNotTerm() TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm()); } -void TermBlack::testIsParameterized() -{ - Term n; - TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&); - Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); - TS_ASSERT_THROWS_NOTHING(x.isParameterized()); -} - void TermBlack::testAndTerm() { Sort bvSort = d_solver.mkBitVectorSort(8); -- cgit v1.2.3