Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.

4 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index cfbadbf32..5fdc549d0 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -459,7 +459,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
 
   if (Theory::isLeafOf(node, theory::THEORY_BV)) {
     // if it is a leaf may ask for fullModel
-    value = getModelFromSatSolver(node, fullModel); 
+    value = getModelFromSatSolver(node, true); 
     Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
     Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); 
     if (!value.isNull()) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 3b54e3794..a103d1f63 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -216,7 +216,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
       // only shared terms could not have been bit-blasted
       Assert (hasBBTerm(var) || isSharedTerm(var));
 
-      Node const_value = getModelFromSatSolver(var, fullModel);
+      Node const_value = getModelFromSatSolver(var, true);
 
       if(const_value != Node()) {
         Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index c821b50cd..b549c329a 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -491,7 +491,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
     // only shared terms could not have been bit-blasted
     Assert (hasBBTerm(var) || isSharedTerm(var));
 
-    Node const_value = getModelFromSatSolver(var, fullModel);
+    Node const_value = getModelFromSatSolver(var, true);
     Assert (const_value.isNull() || const_value.isConst());
     if(const_value != Node()) {
       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 152a335a5..2bcb6ca1b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -349,7 +349,7 @@ Node RewriteRule<SdivEliminate>::apply(TNode node) {
   Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
   Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
 
-  Node a_udiv_b   = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
+  Node a_udiv_b   = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b);
   Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
   
   Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
@@ -377,7 +377,7 @@ Node RewriteRule<SremEliminate>::apply(TNode node) {
   Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
   Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
 
-  Node a_urem_b   = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+  Node a_urem_b   = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b);
   Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
   
   Node result    = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);