summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/term_formula_removal.cpp12
-rw-r--r--src/theory/quantifiers/sygus_inference.cpp2
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h4
-rw-r--r--src/theory/term_registration_visitor.cpp40
-rw-r--r--src/theory/theory.h5
-rw-r--r--src/theory/theory_engine.cpp12
6 files changed, 42 insertions, 33 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 250c21202..fc10d2b4b 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -215,8 +215,11 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
// The representation is now the skolem
return skolem;
}
-
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+
+ if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
+ || node.getKind() == kind::LAMBDA
+ || node.getKind() == kind::CHOICE)
+ {
// Remember if we're inside a quantifier
inQuant = true;
}else if( !inTerm && hasNestedTermChildren( node ) ){
@@ -275,7 +278,10 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
return cached.isNull() ? Node(node) : cached;
}
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
+ || node.getKind() == kind::LAMBDA
+ || node.getKind() == kind::CHOICE)
+ {
// Remember if we're inside a quantifier
inQuant = true;
}else if( !inTerm && hasNestedTermChildren( node ) ){
diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp
index 5b995f052..cea992f54 100644
--- a/src/theory/quantifiers/sygus_inference.cpp
+++ b/src/theory/quantifiers/sygus_inference.cpp
@@ -192,7 +192,7 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
// sygus attribute to mark the conjecture as a sygus conjecture
Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl;
- Node sygusVar = nm->mkBoundVar("sygus", nm->booleanType());
+ Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
SygusAttribute ca;
sygusVar.setAttribute(ca, true);
Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4f87f6aae..4bb28fe79 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -58,10 +58,6 @@ class TheoryQuantifiers : public Theory {
Node n,
std::vector<Node> node_values,
std::string str_value) override;
- bool ppDontRewriteSubterm(TNode atom) override
- {
- return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS;
- }
private:
void assertUniversal( Node n );
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 1e1a2e8e6..eae5578cf 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -35,15 +35,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
- if( ( parent.getKind() == kind::FORALL ||
- parent.getKind() == kind::EXISTS ||
- parent.getKind() == kind::REWRITE_RULE ||
- parent.getKind() == kind::SEP_STAR ||
- parent.getKind() == kind::SEP_WAND ||
- ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
- // parent.getKind() == kind::CARDINALITY_CONSTRAINT
- ) &&
- current != parent ) {
+ if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
+ || parent.getKind() == kind::LAMBDA
+ || parent.getKind() == kind::CHOICE
+ || parent.getKind() == kind::REWRITE_RULE
+ || parent.getKind() == kind::SEP_STAR
+ || parent.getKind() == kind::SEP_WAND
+ || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
+ // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+ )
+ && current != parent)
+ {
Debug("register::internal") << "quantifier:true" << std::endl;
return true;
}
@@ -179,15 +181,17 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
- if( ( parent.getKind() == kind::FORALL ||
- parent.getKind() == kind::EXISTS ||
- parent.getKind() == kind::REWRITE_RULE ||
- parent.getKind() == kind::SEP_STAR ||
- parent.getKind() == kind::SEP_WAND ||
- ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
- // parent.getKind() == kind::CARDINALITY_CONSTRAINT
- ) &&
- current != parent ) {
+ if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
+ || parent.getKind() == kind::LAMBDA
+ || parent.getKind() == kind::CHOICE
+ || parent.getKind() == kind::REWRITE_RULE
+ || parent.getKind() == kind::SEP_STAR
+ || parent.getKind() == kind::SEP_WAND
+ || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
+ // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+ )
+ && current != parent)
+ {
Debug("register::internal") << "quantifier:true" << std::endl;
return true;
}
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f38cda90a..2f7ce6999 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -553,11 +553,6 @@ public:
virtual Node ppRewrite(TNode atom) { return atom; }
/**
- * Don't preprocess subterm of this term
- */
- virtual bool ppDontRewriteSubterm(TNode atom) { return false; }
-
- /**
* Notify preprocessed assertions. Called on new assertions after
* preprocessing before they are asserted to theory engine.
*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index de71a8b5e..38885db85 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -394,6 +394,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
}
// the atom should not have free variables
+ Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
+ << std::endl;
Assert(!preprocessed.hasFreeVar());
// Pre-register the terms in the atom
Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
@@ -1056,9 +1058,15 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) {
Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
Node newTerm;
- if (theoryOf(term)->ppDontRewriteSubterm(term)) {
+ // do not rewrite inside quantifiers
+ if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS
+ || term.getKind() == kind::CHOICE
+ || term.getKind() == kind::LAMBDA)
+ {
newTerm = Rewriter::rewrite(term);
- } else {
+ }
+ else
+ {
NodeBuilder<> newNode(term.getKind());
if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
newNode << term.getOperator();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback