diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:04:51 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:07:39 -0600 |
| commit | 841b7951f41f399859afab13a81e04599308da61 (patch) | |
| tree | 8c6eb70b498b0a01f00c1a77b96d00ff2f61c21b /src/theory/quantifiers/model_builder.cpp | |
| parent | 18fed5592fb769d12ba2901a0fdc00c5c02863b9 (diff) | |
Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index cb63ccd45..493d54b53 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -929,13 +929,13 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, Node ret; if( n.getKind()==NOT ){ ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); - }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){ + }else if( n.getKind()==OR || n.getKind()==AND ){ //whether we only need to find one or all bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity ); std::vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i]; - Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i]; + Node fnc = fn[i]; + Node nc = n[i]; Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); if( nn.isNull() && !favorPol ){ //cannot make selection formula @@ -993,8 +993,8 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){ ret = mkAndSelectionFormula( nc[0], nc[1] ); } - }else if( n.getKind()==IFF || n.getKind()==XOR ){ - bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF; + }else if( n.getKind()==IFF ){ + bool opPol = !polarity; for( int p=0; p<2; p++ ){ Node nn[2]; for( int i=0; i<2; i++ ){ |