diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
| commit | cc01e2119801bbd4fd99548b79c297fa57a1977d (patch) | |
| tree | cf9c64efbc286089a898d93abb3150e79138e5a7 /src/theory/quantifiers/ambqi_builder.h | |
| parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) | |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.h')
| -rwxr-xr-x | src/theory/quantifiers/ambqi_builder.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index def074177..784fa5093 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -62,6 +62,7 @@ public: void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
+ terms.resize( q[0].getNumChildren() );
return addInstantiations( m, qe, q, terms, inst, 0 );
}
bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
|