diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-05-19 16:24:59 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 16:24:59 -0500 |
commit | c8f149fa83fa16f821f37687fedfa778808809bd (patch) | |
tree | 8808ec522b58c0d8273280923b984a72e0b7bb29 /src/theory/builtin | |
parent | 6bb98062a5578d126db6a3e8cdca083881893b32 (diff) |
Renamed operator CHOICE to WITNESS (#4207)
Renamed operator CHOICE to WITNESS, and removed it from the front end
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 12 |
4 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 4d5e95119..a11354b1a 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -298,7 +298,7 @@ operator SEXPR 0: "a symbolic expression (any arity)" operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" -operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" +operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ @@ -329,7 +329,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule -typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule +typerule WITNESS ::CVC4::theory::builtin::WitnessTypeRule # lambda expressions that are isomorphic to array constants can be considered constants construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index b9d05b833..1667e5505 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -46,7 +46,7 @@ void TheoryBuiltin::finishInit() // choice nodes are not evaluated in getModelValue TheoryModel* theoryModel = d_valuation.getModel(); Assert(theoryModel != nullptr); - theoryModel->setUnevaluatedKind(kind::CHOICE); + theoryModel->setUnevaluatedKind(kind::WITNESS); } } // namespace builtin diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index dd6d434ca..d8175dd60 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -92,7 +92,7 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { } return RewriteResponse(REWRITE_DONE, node); } - else if (node.getKind() == kind::CHOICE) + else if (node.getKind() == kind::WITNESS) { if (node[1].getKind() == kind::EQUAL) { diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index a3d1776e1..28d6c9037 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -159,7 +159,7 @@ class LambdaTypeRule { } };/* class LambdaTypeRule */ -class ChoiceTypeRule +class WitnessTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, @@ -169,14 +169,14 @@ class ChoiceTypeRule if (n[0].getType(check) != nodeManager->boundVarListType()) { std::stringstream ss; - ss << "expected a bound var list for CHOICE expression, got `" + ss << "expected a bound var list for WITNESS expression, got `" << n[0].getType().toString() << "'"; throw TypeCheckingExceptionPrivate(n, ss.str()); } if (n[0].getNumChildren() != 1) { std::stringstream ss; - ss << "expected a bound var list with one argument for CHOICE expression"; + ss << "expected a bound var list with one argument for WITNESS expression"; throw TypeCheckingExceptionPrivate(n, ss.str()); } if (check) @@ -185,14 +185,14 @@ class ChoiceTypeRule if (!rangeType.isBoolean()) { std::stringstream ss; - ss << "expected a body of a CHOICE expression to have Boolean type"; + ss << "expected a body of a WITNESS expression to have Boolean type"; throw TypeCheckingExceptionPrivate(n, ss.str()); } } - // The type of a choice function is the type of its bound variable. + // The type of a witness function is the type of its bound variable. return n[0][0].getType(); } -}; /* class ChoiceTypeRule */ +}; /* class WitnessTypeRule */ class SortProperties { public: |