summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp79
-rw-r--r--src/theory/quantifiers/inst_match.cpp2
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp22
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp7
-rw-r--r--src/theory/quantifiers/options5
-rw-r--r--src/theory/quantifiers/quant_util.h2
-rw-r--r--src/theory/quantifiers/trigger.cpp35
-rw-r--r--src/theory/quantifiers/trigger.h3
-rw-r--r--src/theory/quantifiers_engine.cpp12
-rw-r--r--src/theory/quantifiers_engine.h6
-rw-r--r--src/util/ite_removal.cpp45
-rw-r--r--src/util/ite_removal.h2
12 files changed, 152 insertions, 68 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8eb6664ca..e7b3daa2b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1427,17 +1427,27 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
return node;
}
+
+struct ContainsQuantAttributeId {};
+typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
+
// check if the given node contains a universal quantifier
static bool containsQuantifiers(Node n) {
- if(n.getKind() == kind::FORALL) {
+ if( n.hasAttribute(ContainsQuantAttribute()) ){
+ return n.getAttribute(ContainsQuantAttribute())==1;
+ } else if(n.getKind() == kind::FORALL) {
return true;
} else {
- for(unsigned i = 0; i < n.getNumChildren(); ++i) {
- if(containsQuantifiers(n[i])) {
- return true;
+ bool cq = false;
+ for( unsigned i = 0; i < n.getNumChildren(); ++i ){
+ if( containsQuantifiers(n[i]) ){
+ cq = true;
+ break;
}
}
- return false;
+ ContainsQuantAttribute cqa;
+ n.setAttribute(cqa, cq ? 1 : 0);
+ return cq;
}
}
@@ -1498,43 +1508,36 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
}
}else{
//check if it contains a quantifier as a subterm
- bool containsQuant = false;
- if( n.getType().isBoolean() ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( containsQuantifiers( n[i] ) ){
- containsQuant = true;
- break;
- }
- }
- }
//if so, we will write this node
- if( containsQuant ){
- if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
- Node nn;
- //must remove structure
- if( n.getKind()==kind::ITE ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
- }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
- }else if( n.getKind()==kind::IMPLIES ){
- nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
- }
- return preSkolemizeQuantifiers( nn, polarity, fvs );
- }else{
- Assert( n.getKind() == kind::AND || n.getKind() == kind::OR );
- vector< Node > children;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+ if( containsQuantifiers( n ) ){
+ if( n.getType().isBoolean() ){
+ if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
+ Node nn;
+ //must remove structure
+ if( n.getKind()==kind::ITE ){
+ nn = NodeManager::currentNM()->mkNode( kind::AND,
+ NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+ NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+ }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+ nn = NodeManager::currentNM()->mkNode( kind::AND,
+ NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+ NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+ }else if( n.getKind()==kind::IMPLIES ){
+ nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+ }
+ return preSkolemizeQuantifiers( nn, polarity, fvs );
+ }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+ vector< Node > children;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ //must pull ite's
}
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
}
- }else{
- return n;
}
+ return n;
}
}
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 85a96f90a..5a80512cd 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -140,7 +140,7 @@ void InstMatch::set(TNode var, TNode n){
//var.getType() == n.getType()
!n.getType().isSubtypeOf( var.getType() ) ){
Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
- Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ;
+ Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
Assert(false);
}
d_map[var] = n;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 5484e25e9..dd8588b52 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -74,7 +74,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
int childMatchPolicy = MATCH_GEN_DEFAULT;
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
+ if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
d_children.push_back( cimg );
d_children_index.push_back( i );
@@ -115,7 +115,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
}else{
d_cg = new CandidateGeneratorQueue;
- if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
+ if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
//Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
@@ -155,14 +155,20 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
//first, check if ground arguments are not equal, or a match is in conflict
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !m.setMatch( q, d_match_pattern[i], t[i] ) ){
+ if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+ Node vv = d_match_pattern[i];
+ Node tt = t[i];
+ if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+ vv = d_match_pattern[i][0];
+ tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] ));
+ }
+ if( !m.setMatch( q, vv, tt ) ){
//match is in conflict
- Debug("matching-debug") << "Match in conflict " << t[i] << " and "
- << d_match_pattern[i] << " because "
- << m.get(d_match_pattern[i])
+ Debug("matching-debug") << "Match in conflict " << tt << " and "
+ << vv << " because "
+ << m.get(vv)
<< std::endl;
- Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl;
+ Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl;
success = false;
break;
}
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 3f5cc7666..0915f59a5 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -145,6 +145,10 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
if( gen ){
generateTriggers( f, effort, e, status );
}
+ //if( e==4 ){
+ // d_processed_trigger.clear();
+ // d_quantEngine->getEqualityQuery()->setLiberal( true );
+ //}
Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
//Notice() << "Try auto-generated triggers..." << std::endl;
for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
@@ -171,6 +175,9 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
}
}
}
+ //if( e==4 ){
+ // d_quantEngine->getEqualityQuery()->setLiberal( false );
+ //}
Debug("quant-uf-strategy") << "done." << std::endl;
//Notice() << "done" << std::endl;
return status;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 7a3687dd5..222fc4425 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -36,7 +36,8 @@ option cnfQuant --cnf-quant bool :default false
# forall x. P( x ) => f( S( x ) ) = x
option preSkolemQuant --pre-skolem-quant bool :default false
apply skolemization eagerly to bodies of quantified formulas
-
+option iteRemoveQuant --ite-remove-quant bool :default false
+ apply ite removal to bodies of quantifiers
# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
perform aggressive miniscoping for quantifiers
@@ -48,7 +49,7 @@ option macrosQuant --macros-quant bool :default false
option smartTriggers /--disable-smart-triggers bool :default true
disable smart triggers
# Whether to use relevent triggers
-option relevantTriggers --relevant-triggers bool :default true
+option relevantTriggers /--disable-relevant-triggers bool :default true
prefer triggers that are more relevant based on SInE style analysis
# Whether to consider terms in the bodies of quantifiers for matching
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 85602dbab..0b4f2654b 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -91,6 +91,8 @@ public:
virtual eq::EqualityEngine* getEngine() = 0;
/** get the equivalence class of a */
virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+
+ virtual void setLiberal( bool l ) = 0;
};/* class EqualityQuery */
}
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index cff28f243..125829e06 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -226,17 +226,24 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
bool Trigger::isUsable( Node n, Node f ){
if( n.getAttribute(InstConstantAttribute())==f ){
- if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
- std::map< Node, Node > coeffs;
- return getPatternArithmetic( f, n, coeffs );
- }else{
+ if( isAtomicTrigger( n ) ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
if( !isUsable( n[i], f ) ){
return false;
}
}
return true;
+ }else if( n.getKind()==INST_CONSTANT ){
+ return true;
+ }else{
+ std::map< Node, Node > coeffs;
+ if( isArithmeticTrigger( f, n, coeffs ) ){
+ return true;
+ }else if( isBooleanTermTrigger( n ) ){
+ return true;
+ }
}
+ return false;
}else{
return true;
}
@@ -368,7 +375,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
}
}
-bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
+bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){
if( n.getKind()==PLUS ){
Assert( coeffs.empty() );
NodeBuilder<> t(kind::PLUS);
@@ -381,7 +388,7 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
coeffs.clear();
return false;
}
- }else if( !getPatternArithmetic( f, n[i], coeffs ) ){
+ }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){
coeffs.clear();
return false;
}
@@ -413,6 +420,22 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
return false;
}
+bool Trigger::isBooleanTermTrigger( Node n ) {
+ if( n.getKind()==ITE ){
+ //check for boolean term converted to ITE
+ if( n[0].getKind()==INST_CONSTANT &&
+ n[1].getKind()==CONST_BITVECTOR &&
+ n[2].getKind()==CONST_BITVECTOR ){
+ if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
+ n[1].getConst<BitVector>().toInteger()==1 &&
+ n[2].getConst<BitVector>().toInteger()==0 ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
if( nodes.empty() ){
return d_tr;
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 93731283b..9ecac0120 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -109,7 +109,8 @@ public:
static bool isAtomicTrigger( Node n );
static bool isSimpleTrigger( Node n );
/** get pattern arithmetic */
- static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
+ static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs );
+ static bool isBooleanTermTrigger( Node n );
inline void toStream(std::ostream& out) const {
out << "TRIGGER( ";
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a11cc85c0..f12143bbe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -583,12 +583,16 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
return true;
}else{
eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areEqual( a, b ) ){
- return true;
+ if( d_liberal ){
+ return true;//!areDisequal( a, b );
+ }else{
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areEqual( a, b ) ){
+ return true;
+ }
}
+ return false;
}
- return false;
}
}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 9f520f420..5f288a186 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -272,6 +272,8 @@ private:
std::map< Node, int > d_rep_score;
/** reset count */
int d_reset_count;
+
+ bool d_liberal;
private:
/** node contains */
Node getInstance( Node n, std::vector< Node >& eqc );
@@ -280,7 +282,7 @@ private:
/** choose rep based on sort inference */
bool optInternalRepSortInference();
public:
- EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
+ EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
~EqualityQueryQuantifiersEngine(){}
/** reset */
void reset();
@@ -296,6 +298,8 @@ public:
not contain instantiation constants, if such a term exists.
*/
Node getInternalRepresentative( Node a, Node f, int index );
+
+ void setLiberal( bool l ) { d_liberal = l; }
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory namespace */
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 240e5a0cf..de7ae2e97 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -19,6 +19,7 @@
#include "util/ite_removal.h"
#include "theory/rewriter.h"
#include "expr/command.h"
+#include "theory/quantifiers/options.h"
using namespace CVC4;
using namespace std;
@@ -28,12 +29,13 @@ namespace CVC4 {
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- output[i] = run(output[i], output, iteSkolemMap);
+ std::vector<Node> quantVar;
+ output[i] = run(output[i], output, iteSkolemMap, quantVar);
}
}
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap) {
+ IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
@@ -50,8 +52,23 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
if(!nodeType.isBoolean()) {
+ Node skolem;
// Make the skolem to represent the ITE
- Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+ if( quantVar.empty() ){
+ skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+ }else{
+ //if in the scope of free variables, make a skolem operator
+ vector< TypeNode > argTypes;
+ for( size_t i=0; i<quantVar.size(); i++ ){
+ argTypes.push_back( quantVar[i].getType() );
+ }
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
+ Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
+ vector< Node > funcArgs;
+ funcArgs.push_back( op );
+ funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
+ skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+ }
// The new assertion
Node newAssertion =
@@ -63,7 +80,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
d_iteCache[node] = skolem;
// Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap);
+ newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
+
+ if( !quantVar.empty() ){
+ //if in the scope of free variables, it is a quantified assertion
+ vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
+ children.push_back( newAssertion );
+ newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
+ }
+
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
@@ -73,9 +99,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
}
// If not an ITE, go deep
- if( node.getKind() != kind::FORALL &&
+ if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
node.getKind() != kind::EXISTS &&
node.getKind() != kind::REWRITE_RULE ) {
+ std::vector< Node > newQuantVar;
+ newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
+ if( node.getKind()==kind::FORALL ){
+ for( size_t i=0; i<node[0].getNumChildren(); i++ ){
+ newQuantVar.push_back( node[0][i] );
+ }
+ }
vector<Node> newChildren;
bool somethingChanged = false;
if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -83,7 +116,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
}
// Remove the ITEs from the children
for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap);
+ Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
somethingChanged |= (newChild != *it);
newChildren.push_back(newChild);
}
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 77e9c39db..6c0c74cd4 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -55,7 +55,7 @@ public:
* ite created in conjunction with that skolem variable.
*/
Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap);
+ IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
};/* class RemoveTTE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback