diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/theory/quantifiers/ambqi_builder.h | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.h')
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 784fa5093..349073cb4 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -36,7 +36,7 @@ private: std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
std::vector< unsigned >& entry, std::vector< bool >& entry_def );
void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
- void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );
+ void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
void apply_ucompose( FirstOrderModelAbs * m, TNode q,
std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
@@ -59,7 +59,7 @@ public: void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
- void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
+ void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
terms.resize( q[0].getNumChildren() );
@@ -73,7 +73,7 @@ public: void negate();
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
static bool isSimple( unsigned n );
- static unsigned getId( unsigned n, unsigned start=0 );
+ static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
//for debugging
|