This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
#else
#define Assert(cond) \
CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__)
-#endif /* CVC4_DEBUG */
+#endif
class AssertArgumentException : public Exception
{
# include <sys/resource.h>
#endif /* ! __WIN32__ */
-#include <cassert>
#include <iostream>
#include <memory>
#include <string>
#include "main/interactive_shell.h"
#include <algorithm>
-#include <cassert>
#include <cstdlib>
#include <iostream>
#include <set>
#endif /* HAVE_LIBEDITLINE */
#include "api/cvc4cpp.h"
+#include "base/check.h"
#include "base/output.h"
#include "expr/symbol_manager.h"
#include "options/language.h"
Debug("interactive") << "Input now '" << input << line << "'" << endl
<< flush;
- assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
+ Assert(!(d_in.fail() && !d_in.eof()) || line.empty());
/* Check for failure. */
if(d_in.fail() && !d_in.eof()) {
/* This should only happen if the input line was empty. */
- assert( line.empty() );
+ Assert(line.empty());
d_in.clear();
}
{
/* Extract the newline delimiter from the stream too */
int c CVC4_UNUSED = d_in.get();
- assert(c == '\n');
+ Assert(c == '\n');
Debug("interactive") << "Next char is '" << (char)c << "'" << endl
<< flush;
}
#include <antlr3.h>
#include <limits.h>
+#include "base/check.h"
#include "base/output.h"
#include "parser/antlr_line_buffered_input.h"
#include "parser/bounded_token_buffer.h"
d_input(input),
d_inputString(inputString),
d_line_buffer(line_buffer) {
- assert( input != NULL );
+ Assert(input != NULL);
input->fileName = input->strFactory->newStr8(input->strFactory, (pANTLR3_UINT8)name.c_str());
}
throw InputStreamException("Stream input failed: " + name);
}
ptrdiff_t offset = cp - basep;
- assert(offset >= 0);
- assert(offset <= std::numeric_limits<uint32_t>::max());
+ Assert(offset >= 0);
+ Assert(offset <= std::numeric_limits<uint32_t>::max());
inputStringCopy = (pANTLR3_UINT8)basep;
inputStream = newAntrl3InPlaceStream(inputStringCopy, (uint32_t) offset, name);
}
const std::string& name)
{
size_t input_size = input.size();
- assert(input_size <= std::numeric_limits<uint32_t>::max());
+ Assert(input_size <= std::numeric_limits<uint32_t>::max());
// Ownership of input_duplicate is transferred to the AntlrInputStream.
pANTLR3_UINT8 input_duplicate = (pANTLR3_UINT8) strdup(input.c_str());
void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
- assert(lexer!=NULL);
+ Assert(lexer != NULL);
Parser *parser = (Parser*)(lexer->super);
- assert(parser!=NULL);
+ Assert(parser != NULL);
AntlrInput *input = (AntlrInput*) parser->getInput();
- assert(input!=NULL);
+ Assert(input != NULL);
/* Call the error display routine *if* there's not already a
* parse error pending. If a parser error is pending, this
#ifndef CVC4__PARSER__ANTLR_INPUT_H
#define CVC4__PARSER__ANTLR_INPUT_H
-#include "cvc4parser_private.h"
-
#include <antlr3.h>
+
#include <iostream>
#include <sstream>
#include <stdexcept>
#include <string>
#include <vector>
-#include <cassert>
+#include "base/check.h"
#include "base/output.h"
+#include "cvc4parser_private.h"
#include "parser/bounded_token_buffer.h"
#include "parser/input.h"
#include "parser/line_buffer.h"
ANTLR3_MARKER start = token->getStartIndex(token);
// Its the last character of the token (not the one just after)
ANTLR3_MARKER end = token->getStopIndex(token);
- assert( start < end );
+ Assert(start < end);
if( index > (size_t) end - start ) {
std::stringstream ss;
ss << "Out-of-bounds substring index: " << index;
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-
#include <antlr3.h>
+
#include <sstream>
+#include "base/check.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
// Dig the CVC4 objects out of the ANTLR3 mess
pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
- assert(antlr3Parser!=NULL);
+ Assert(antlr3Parser != NULL);
Parser *parser = (Parser*)(antlr3Parser->super);
- assert(parser!=NULL);
+ Assert(parser != NULL);
AntlrInput *input = (AntlrInput*) parser->getInput() ;
- assert(input!=NULL);
+ Assert(input != NULL);
// Signal we are in error recovery now
recognizer->state->errorRecovery = ANTLR3_TRUE;
}
}
} else {
- assert(false);//("Parse error with empty set of expected tokens.");
+ Assert(false); //("Parse error with empty set of expected tokens.");
}
}
break;
// then we are just going to report what we know about the
// token.
//
- assert(false);//("Unexpected exception in parser.");
+ Assert(false); //("Unexpected exception in parser.");
break;
}
#include "parser/antlr_line_buffered_input.h"
#include <antlr3.h>
+
#include <iostream>
#include <string>
-#include <cassert>
+#include "base/check.h"
#include "base/output.h"
namespace CVC4 {
pANTLR3_INPUT_STREAM input = ((pANTLR3_INPUT_STREAM)(is->super));
// Check that we are not seeking backwards.
- assert(!((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)
+ Assert(!((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)
->line_buffer->isPtrBefore(
(uint8_t*)seekPoint, input->line, input->charPositionInLine));
static ANTLR3_UINT32 bufferedInputSize(pANTLR3_INPUT_STREAM input) {
// Not supported for this type of stream
- assert(false);
+ Assert(false);
return 0;
}
static void bufferedInputSetNewLineChar(pANTLR3_INPUT_STREAM input,
ANTLR3_UINT32 newlineChar) {
// Not supported for this type of stream
- assert(false);
+ Assert(false);
}
static void bufferedInputSetUcaseLA(pANTLR3_INPUT_STREAM input,
ANTLR3_BOOLEAN flag) {
// Not supported for this type of stream
- assert(false);
+ Assert(false);
}
pANTLR3_INPUT_STREAM antlr3LineBufferedStreamNew(std::istream& in,
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#include "parser/bounded_token_buffer.h"
+
#include <antlr3commontoken.h>
#include <antlr3lexer.h>
#include <antlr3tokenstream.h>
-#include "parser/bounded_token_buffer.h"
-#include <cassert>
+#include "base/check.h"
namespace CVC4 {
namespace parser {
pBOUNDED_TOKEN_BUFFER buffer;
pANTLR3_COMMON_TOKEN_STREAM stream;
- assert(k > 0);
+ Assert(k > 0);
/* Memory for the interface structure */
buffer =
buffer = (pBOUNDED_TOKEN_BUFFER) cts->super;
/* k must be in the range [-buffer->k..buffer->k] */
- assert( k <= (ANTLR3_INT32)buffer->k
- && -k <= (ANTLR3_INT32)buffer->k );
+ Assert(k <= (ANTLR3_INT32)buffer->k && -k <= (ANTLR3_INT32)buffer->k);
if(k == 0) {
return NULL;
/* Initialize the buffer on our first call. */
if( __builtin_expect( (buffer->empty == ANTLR3_TRUE), false ) ) {
- assert( buffer->tokenBuffer != NULL );
+ Assert(buffer->tokenBuffer != NULL);
buffer->tokenBuffer[ 0 ] = nextToken(buffer);
buffer->maxIndex = 0;
buffer->currentIndex = 0;
kIndex = buffer->currentIndex + k - 1;
} else {
/* Can't look behind more tokens than we've consumed. */
- assert( -k <= (ANTLR3_INT32)buffer->currentIndex );
+ Assert(-k <= (ANTLR3_INT32)buffer->currentIndex);
/* look-behind token k is at offset -k */
kIndex = buffer->currentIndex + k;
}
static pANTLR3_COMMON_TOKEN
get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i)
{
- assert(false);// unimplemented
- return NULL;
+ Assert(false); // unimplemented
+ return NULL;
}
static pANTLR3_TOKEN_SOURCE
static pANTLR3_STRING
toString (pANTLR3_TOKEN_STREAM ts)
{
- assert(false);// unimplemented
+ Assert(false); // unimplemented
return NULL;
}
static pANTLR3_STRING
toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
{
- assert(false);// unimplemented
+ Assert(false); // unimplemented
return NULL;
}
static pANTLR3_STRING
toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
{
- assert(false);// unimplemented
+ Assert(false); // unimplemented
return NULL;
}
static ANTLR3_UINT32
dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
{
- assert(false);
+ Assert(false);
return 0;
}
static ANTLR3_MARKER
dbgMark (pANTLR3_INT_STREAM is)
{
- assert(false);
+ Assert(false);
return 0;
}
static ANTLR3_UINT32
size (pANTLR3_INT_STREAM is)
{
- assert(false);
+ Assert(false);
return 0;
}
return buffer->currentIndex;
}
-static void
-dbgRewindLast (pANTLR3_INT_STREAM is)
-{
- assert(false);
-}
-static void
-rewindLast (pANTLR3_INT_STREAM is)
-{
- assert(false);
-}
+static void dbgRewindLast(pANTLR3_INT_STREAM is) { Assert(false); }
+static void rewindLast(pANTLR3_INT_STREAM is) { Assert(false); }
static void
rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
{
static void
dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
{
- assert(false);
+ Assert(false);
}
static void
static void
dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
{
- assert(false);
+ Assert(false);
}
static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
const std::vector<CVC4::api::Term>& expressions,
const std::vector<unsigned>& operators,
unsigned startIndex, unsigned stopIndex) {
- assert(expressions.size() == operators.size() + 1);
- assert(startIndex < expressions.size());
- assert(stopIndex < expressions.size());
- assert(startIndex <= stopIndex);
+ Assert(expressions.size() == operators.size() + 1);
+ Assert(startIndex < expressions.size());
+ Assert(stopIndex < expressions.size());
+ Assert(startIndex <= stopIndex);
if(stopIndex == startIndex) {
return expressions[startIndex];
@parser::includes {
-#include <cassert>
#include <memory>
+#include "base/check.h"
#include "options/set_language.h"
#include "parser/antlr_tracing.h"
#include "parser/parser.h"
// like e.g. FORALL(x:INT = 4): [...]
PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
}
- assert(!idList.empty());
+ Assert(!idList.empty());
api::Term fterm = f;
std::vector<api::Term> formals;
if (f.getKind()==api::LAMBDA)
/* a type, possibly a function */
: restrictedTypePossiblyFunctionLHS[t,check,lhs]
{ if(lhs) {
- assert(t.isTuple());
+ Assert(t.isTuple());
args = t.getTupleSorts();
} else {
args.push_back(t);
}
/* bitvector literals */
| HEX_LITERAL
- { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
+ { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
f = SOLVER->mkBitVector(hexString, 16);
}
| BINARY_LITERAL
- { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
+ { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
f = SOLVER->mkBitVector(binString, 2);
}
| PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
{ std::vector< std::pair<std::string, api::Sort> > typeIds;
- assert(names.size() == args.size());
+ Assert(names.size() == args.size());
for(unsigned i = 0; i < names.size(); ++i) {
typeIds.push_back(std::make_pair(names[i], args[i].getSort()));
}
#include <antlr3.h>
+#include "base/check.h"
#include "parser/antlr_input.h"
-#include "parser/parser_exception.h"
#include "parser/cvc/CvcLexer.h"
#include "parser/cvc/CvcParser.h"
+#include "parser/parser_exception.h"
namespace CVC4 {
namespace parser {
CvcInput::CvcInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream,6) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- assert( input != NULL );
+ Assert(input != NULL);
d_pCvcLexer = CvcLexerNew(input);
if( d_pCvcLexer == NULL ) {
setAntlr3Lexer( d_pCvcLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- assert( tokenStream != NULL );
+ Assert(tokenStream != NULL);
d_pCvcParser = CvcParserNew(tokenStream);
if( d_pCvcParser == NULL ) {
#include "parser/line_buffer.h"
-#include <cassert>
#include <cstring>
#include <iostream>
#include <string>
+#include "base/check.h"
+
namespace CVC4 {
namespace parser {
if (!readToLine(line)) {
return NULL;
}
- assert(pos_in_line < d_sizes[line]);
+ Assert(pos_in_line < d_sizes[line]);
return d_lines[line] + pos_in_line;
}
return getPtrWithOffset(line + 1, 0,
offset - (d_sizes[line] - pos_in_line - 1));
}
- assert(pos_in_line + offset < d_sizes[line]);
+ Assert(pos_in_line + offset < d_sizes[line]);
return d_lines[line] + pos_in_line + offset;
}
#include "parser/parser.h"
-#include <cassert>
#include <clocale>
#include <fstream>
#include <iostream>
#include <unordered_set>
#include "api/cvc4cpp.h"
+#include "base/check.h"
#include "base/output.h"
#include "expr/kind.h"
#include "options/options.h"
api::Term Parser::getSymbol(const std::string& name, SymbolType type)
{
checkDeclaration(name, CHECK_DECLARED, type);
- assert(isDeclared(name, type));
- assert(type == SYM_VARIABLE);
+ Assert(isDeclared(name, type));
+ Assert(type == SYM_VARIABLE);
// Functions share var namespace
return d_symtab->lookup(name);
}
+void Parser::forceLogic(const std::string& logic)
+{
+ Assert(!d_logicIsForced);
+ d_logicIsForced = true;
+ d_forcedLogic = logic;
+}
+
api::Term Parser::getVariable(const std::string& name)
{
return getSymbol(name, SYM_VARIABLE);
api::Term Parser::getExpressionForNameAndType(const std::string& name,
api::Sort t)
{
- assert(isDeclared(name));
+ Assert(isDeclared(name));
// first check if the variable is declared and not overloaded
api::Term expr = getVariable(name);
if(expr.isNull()) {
}
}
// now, post-process the expression
- assert( !expr.isNull() );
+ Assert(!expr.isNull());
api::Sort te = expr.getSort();
if (te.isConstructor() && te.getConstructorArity() == 0)
{
api::Sort Parser::getSort(const std::string& name)
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
- assert(isDeclared(name, SYM_SORT));
+ Assert(isDeclared(name, SYM_SORT));
api::Sort t = d_symtab->lookupType(name);
return t;
}
const std::vector<api::Sort>& params)
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
- assert(isDeclared(name, SYM_SORT));
+ Assert(isDeclared(name, SYM_SORT));
api::Sort t = d_symtab->lookupType(name, params);
return t;
}
size_t Parser::getArity(const std::string& sort_name) {
checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
- assert(isDeclared(sort_name, SYM_SORT));
+ Assert(isDeclared(sort_name, SYM_SORT));
return d_symtab->lookupArity(sort_name);
}
ss << ", maybe the symbol has already been defined?";
parseError(ss.str());
}
- assert(isDeclared(name));
+ Assert(isDeclared(name));
}
void Parser::defineType(const std::string& name,
{
if (skipExisting && isDeclared(name, SYM_SORT))
{
- assert(d_symtab->lookupType(name) == type);
+ Assert(d_symtab->lookupType(name) == type);
return;
}
d_symtab->bindType(name, type, levelZero);
- assert(isDeclared(name, SYM_SORT));
+ Assert(isDeclared(name, SYM_SORT));
}
void Parser::defineType(const std::string& name,
bool levelZero)
{
d_symtab->bindType(name, params, type, levelZero);
- assert(isDeclared(name, SYM_SORT));
+ Assert(isDeclared(name, SYM_SORT));
}
void Parser::defineParameterizedType(const std::string& name,
std::vector<api::Sort> types =
d_solver->mkDatatypeSorts(datatypes, d_unresolved);
- assert(datatypes.size() == types.size());
+ Assert(datatypes.size() == types.size());
bool globalDecls = d_symman->getGlobalDeclarations();
for (unsigned i = 0; i < datatypes.size(); ++i) {
case SYM_SORT:
return d_symtab->isBoundType(name);
}
- assert(false); // Unhandled(type);
+ Assert(false); // Unhandled(type);
return false;
}
case CHECK_NONE:
break;
- default:
- assert(false); // Unhandled(check);
+ default: Assert(false); // Unhandled(check);
}
}
#ifndef CVC4__PARSER__PARSER_H
#define CVC4__PARSER__PARSER_H
-#include <cassert>
#include <list>
#include <set>
#include <string>
implementation optional by returning false by default. */
virtual bool logicIsSet() { return false; }
- virtual void forceLogic(const std::string& logic)
- {
- assert(!d_logicIsForced);
- d_logicIsForced = true;
- d_forcedLogic = logic;
- }
+ virtual void forceLogic(const std::string& logic);
+
const std::string& getForcedLogic() const { return d_forcedLogic; }
bool logicIsForced() const { return d_logicIsForced; }
**/
// This must be included first.
-#include "parser/antlr_input.h"
-
#include "parser/parser_builder.h"
#include <string>
#include "api/cvc4cpp.h"
+#include "base/check.h"
#include "cvc/cvc.h"
#include "options/options.h"
+#include "parser/antlr_input.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "smt2/smt2.h"
input = Input::newFileInput(d_lang, d_filename, d_mmap);
break;
case LINE_BUFFERED_STREAM_INPUT:
- assert( d_streamInput != NULL );
+ Assert(d_streamInput != NULL);
input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
break;
case STREAM_INPUT:
- assert( d_streamInput != NULL );
+ Assert(d_streamInput != NULL);
input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
break;
case STRING_INPUT:
break;
}
- assert(input != NULL);
+ Assert(input != NULL);
Parser* parser = NULL;
switch (d_lang)
#include <memory>
+#include "base/check.h"
#include "parser/antlr_tracing.h"
#include "parser/parse_op.h"
#include "parser/parser.h"
// Bit-vector constants
| HEX_LITERAL
{
- assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
+ Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
atomTerm = SOLVER->mkBitVector(hexStr, 16);
}
| BINARY_LITERAL
{
- assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
+ Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
atomTerm = SOLVER->mkBitVector(binStr, 2);
}
{
// Handle SMT-LIB >=2.5 standard escape '""'.
++q;
- assert(*q == '"');
+ Assert(*q == '"');
}
else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
{
// Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
if (*q != '\\' && *q != '"')
{
- assert(*q != '\0');
+ Assert(*q != '\0');
*p++ = '\\';
}
}
api::Term Smt2::mkAbstractValue(const std::string& name)
{
- assert(isAbstractValue(name));
+ Assert(isAbstractValue(name));
// remove the '@'
return d_solver->mkAbstractValue(name.substr(1));
}
{
expr = getExpressionForName(p.d_name);
}
- assert(!expr.isNull());
+ Assert(!expr.isNull());
return expr;
}
#include <antlr3.h>
+#include "base/check.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "parser/smt2/smt2.h"
#include "parser/smt2/Smt2Lexer.h"
#include "parser/smt2/Smt2Parser.h"
+#include "parser/smt2/smt2.h"
namespace CVC4 {
namespace parser {
Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2)
{
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- assert( input != NULL );
+ Assert(input != NULL);
d_pSmt2Lexer = Smt2LexerNew(input);
if( d_pSmt2Lexer == NULL ) {
setAntlr3Lexer( d_pSmt2Lexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- assert( tokenStream != NULL );
+ Assert(tokenStream != NULL);
d_pSmt2Parser = Smt2ParserNew(tokenStream);
if( d_pSmt2Parser == NULL ) {
#include <antlr3.h>
+#include "base/check.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "parser/smt2/sygus_input.h"
#include "parser/smt2/Smt2Lexer.h"
#include "parser/smt2/Smt2Parser.h"
+#include "parser/smt2/sygus_input.h"
namespace CVC4 {
namespace parser {
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- assert( input != NULL );
+ Assert(input != NULL);
d_pSmt2Lexer = Smt2LexerNew(input);
if( d_pSmt2Lexer == NULL ) {
setAntlr3Lexer( d_pSmt2Lexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- assert( tokenStream != NULL );
+ Assert(tokenStream != NULL);
d_pSmt2Parser = Smt2ParserNew(tokenStream);
if( d_pSmt2Parser == NULL ) {
#include <set>
#include "api/cvc4cpp.h"
+#include "base/check.h"
#include "options/options.h"
#include "parser/parser.h"
#include "smt/command.h"
}
// if it has a kind, it's a builtin one and this function should not have been
// called
- assert(p.d_kind == api::NULL_EXPR);
+ Assert(p.d_kind == api::NULL_EXPR);
if (isDeclared(p.d_name))
{ // already appeared
expr = getVariable(p.d_name);
Debug("parser") << "++ " << *i << std::endl;
}
}
- assert(!args.empty());
+ Assert(!args.empty());
// If operator already defined, just build application
if (!p.d_expr.isNull())
{
args[i] = convertRatToUnsorted(args[i]);
}
}
- assert(!v.isNull());
+ Assert(!v.isNull());
checkFunctionLike(v);
kind = getKindForFunction(v);
args.insert(args.begin(), v);
kind = p.d_kind;
isBuiltinKind = true;
}
- assert(kind != api::NULL_EXPR);
+ Assert(kind != api::NULL_EXPR);
const Options& opts = d_solver->getOptions();
// Second phase: apply parse op to the arguments
if (isBuiltinKind)
void Tptp::addFreeVar(api::Term var)
{
- assert(cnf());
+ Assert(cnf());
d_freeVar.push_back(var);
}
std::vector<api::Term> Tptp::getFreeVar()
{
- assert(cnf());
+ Assert(cnf());
std::vector<api::Term> r;
r.swap(d_freeVar);
return r;
return d_nullExpr;
break;
}
- assert(false); // unreachable
+ Assert(false); // unreachable
return d_nullExpr;
}
// "CounterSatisfiable".
if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
d_hasConjecture = true;
- assert(!expr.isNull());
+ Assert(!expr.isNull());
}
if( expr.isNull() ){
return new EmptyCommand("Untreated role for expression");
#ifndef CVC4__PARSER__TPTP_H
#define CVC4__PARSER__TPTP_H
-#include <cassert>
#include <unordered_map>
#include <unordered_set>
#include <antlr3.h>
+#include "base/check.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "parser/tptp/tptp.h"
#include "parser/tptp/TptpLexer.h"
#include "parser/tptp/TptpParser.h"
+#include "parser/tptp/tptp.h"
namespace CVC4 {
namespace parser {
TptpInput::TptpInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- assert( input != NULL );
+ Assert(input != NULL);
d_pTptpLexer = TptpLexerNew(input);
if( d_pTptpLexer == NULL ) {
setAntlr3Lexer( d_pTptpLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- assert( tokenStream != NULL );
+ Assert(tokenStream != NULL);
d_pTptpParser = TptpParserNew(tokenStream);
if( d_pTptpParser == NULL ) {
#include <math.h>
-#include <vector>
#include <iostream>
+#include <vector>
+#include "base/check.h"
#include "base/exception.h"
#include "base/output.h"
#include "options/bv_options.h"
void Solver::attachClause(CRef cr) {
const Clause& clause = ca[cr];
- assert(clause.size() > 1);
+ Assert(clause.size() > 1);
watches[~clause[0]].push(Watcher(cr, clause[1]));
watches[~clause[1]].push(Watcher(cr, clause[0]));
if (clause.learnt())
void Solver::detachClause(CRef cr, bool strict) {
const Clause& clause = ca[cr];
- assert(clause.size() > 1);
+ Assert(clause.size() > 1);
if (strict)
{
bool done = false;
do{
- assert(confl != CRef_Undef); // (otherwise should be UIP)
- Clause& clause = ca[confl];
-
- if (clause.learnt()) claBumpActivity(clause);
+ Assert(confl != CRef_Undef); // (otherwise should be UIP)
+ Clause& clause = ca[confl];
- for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++)
- {
- Lit q = clause[j];
+ if (clause.learnt()) claBumpActivity(clause);
- if (!seen[var(q)] && level(var(q)) > 0)
- {
- varBumpActivity(var(q));
- seen[var(q)] = 1;
- if (level(var(q)) >= decisionLevel())
- pathC++;
- else
- out_learnt.push(q);
- }
+ for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++)
+ {
+ Lit q = clause[j];
+ if (!seen[var(q)] && level(var(q)) > 0)
+ {
+ varBumpActivity(var(q));
+ seen[var(q)] = 1;
+ if (level(var(q)) >= decisionLevel())
+ pathC++;
+ else
+ out_learnt.push(q);
}
+ }
// Select next clause to look at:
while (!seen[var(trail[index--])]);
int top = analyze_toclear.size();
while (analyze_stack.size() > 0){
CRef c_reason = reason(var(analyze_stack.last()));
- assert(c_reason != CRef_Undef);
+ Assert(c_reason != CRef_Undef);
Clause& clause = ca[c_reason];
int c_size = clause.size();
analyze_stack.pop();
* @param out_conflict the conflict in terms of assumptions we are building
*/
void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
- assert (confl_clause != CRef_Undef);
- assert (decisionLevel() == assumptions.size());
- assert (level(var(p)) == assumptions.size());
+ Assert(confl_clause != CRef_Undef);
+ Assert(decisionLevel() == assumptions.size());
+ Assert(level(var(p)) == assumptions.size());
out_conflict.clear();
// we skip p if was a learnt unit
if (x != var(p)) {
if (marker[x] == 2) {
- assert (level(x) > 0);
+ Assert(level(x) > 0);
out_conflict.push(~trail[i]);
}
}
}
seen[x] = 0;
}
- assert(seen[x] == 0);
+ Assert(seen[x] == 0);
}
- assert(out_conflict.size());
+ Assert(out_conflict.size());
}
/*_________________________________________________________________________________________________
Var x = var(trail[i]);
if (seen[x]) {
if (reason(x) == CRef_Undef) {
- assert(marker[x] == 2);
- assert(level(x) > 0);
+ Assert(marker[x] == 2);
+ Assert(level(x) > 0);
if (~trail[i] != p)
{
out_conflict.push(~trail[i]);
}
seen[var(p)] = 0;
- assert (out_conflict.size());
+ Assert(out_conflict.size());
}
void Solver::uncheckedEnqueue(Lit p, CRef from)
{
- assert(value(p) == l_Undef);
- assigns[var(p)] = lbool(!sign(p));
- vardata[var(p)] = mkVarData(from, decisionLevel());
- trail.push_(p);
- if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) {
- if (d_notify) {
- Debug("bvminisat::explain")
- << OUTPUT_TAG << "propagating " << p << std::endl;
- d_notify->notify(p);
- }
+ Assert(value(p) == l_Undef);
+ assigns[var(p)] = lbool(!sign(p));
+ vardata[var(p)] = mkVarData(from, decisionLevel());
+ trail.push_(p);
+ if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1)
+ {
+ if (d_notify)
+ {
+ Debug("bvminisat::explain")
+ << OUTPUT_TAG << "propagating " << p << std::endl;
+ d_notify->notify(p);
}
+ }
}
void Solver::popAssumption() {
// TODO need to somehow mark the assumption as unit in the current context?
// it's not always unit though, but this would be useful for debugging
- // assert(marker[var(p)] == 1);
+ // Assert(marker[var(p)] == 1);
if (decisionLevel() > assumptions.size()) {
cancelUntil(assumptions.size());
Lit false_lit = ~p;
if (clause[0] == false_lit)
clause[0] = clause[1], clause[1] = false_lit;
- assert(clause[1] == false_lit);
+ Assert(clause[1] == false_lit);
i++;
// If 0th watch is true, then clause is already satisfied.
|________________________________________________________________________________________________@*/
bool Solver::simplify()
{
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
- if (!ok || propagate() != CRef_Undef)
- return ok = false;
+ if (!ok || propagate() != CRef_Undef) return ok = false;
- if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
- return true;
+ if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
- d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
+ d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
- // Remove satisfied clauses:
- removeSatisfied(learnts);
- if (remove_satisfied) // Can be turned off.
- removeSatisfied(clauses);
- checkGarbage();
- rebuildOrderHeap();
+ // Remove satisfied clauses:
+ removeSatisfied(learnts);
+ if (remove_satisfied) // Can be turned off.
+ removeSatisfied(clauses);
+ checkGarbage();
+ rebuildOrderHeap();
- simpDB_assigns = nAssigns();
- simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
+ simpDB_assigns = nAssigns();
+ simpDB_props =
+ clauses_literals + learnts_literals; // (shouldn't depend on stats
+ // really, but it will do for now)
- return true;
+ return true;
}
/*_________________________________________________________________________________________________
|________________________________________________________________________________________________@*/
lbool Solver::search(int nof_conflicts, UIP uip)
{
- assert(ok);
- int backtrack_level;
- int conflictC = 0;
- vec<Lit> learnt_clause;
- starts++;
-
- for (;;){
- d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
- CRef confl = propagate();
- if (confl != CRef_Undef){
- // CONFLICT
- conflicts++; conflictC++;
-
- if (decisionLevel() == 0) {
- // can this happen for bv?
- return l_False;
- }
+ Assert(ok);
+ int backtrack_level;
+ int conflictC = 0;
+ vec<Lit> learnt_clause;
+ starts++;
- learnt_clause.clear();
- analyze(confl, learnt_clause, backtrack_level, uip);
+ for (;;)
+ {
+ d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
+ CRef confl = propagate();
+ if (confl != CRef_Undef)
+ {
+ // CONFLICT
+ conflicts++;
+ conflictC++;
- Lit p = learnt_clause[0];
- //bool assumption = marker[var(p)] == 2;
+ if (decisionLevel() == 0)
+ {
+ // can this happen for bv?
+ return l_False;
+ }
- CRef cr = CRef_Undef;
- if (learnt_clause.size() > 1) {
- cr = ca.alloc(learnt_clause, true);
- learnts.push(cr);
- attachClause(cr);
- claBumpActivity(ca[cr]);
- }
+ learnt_clause.clear();
+ analyze(confl, learnt_clause, backtrack_level, uip);
- if (learnt_clause.size() == 1) {
- // learning a unit clause
- }
+ Lit p = learnt_clause[0];
+ // bool assumption = marker[var(p)] == 2;
- // if the uip was an assumption we are unsat
- if (level(var(p)) <= assumptions.size()) {
- for (int i = 0; i < learnt_clause.size(); ++i) {
- assert(level(var(learnt_clause[i])) <= decisionLevel());
- seen[var(learnt_clause[i])] = 1;
- }
+ CRef cr = CRef_Undef;
+ if (learnt_clause.size() > 1)
+ {
+ cr = ca.alloc(learnt_clause, true);
+ learnts.push(cr);
+ attachClause(cr);
+ claBumpActivity(ca[cr]);
+ }
- analyzeFinal(p, conflict);
- Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
- return l_False;
- }
+ if (learnt_clause.size() == 1)
+ {
+ // learning a unit clause
+ }
- if (!CVC4::options::bvEagerExplanations()) {
- // check if uip leads to a conflict
- if (backtrack_level < assumptions.size()) {
- cancelUntil(assumptions.size());
- uncheckedEnqueue(p, cr);
-
- CRef new_confl = propagate();
- if (new_confl != CRef_Undef) {
- // we have a conflict we now need to explain it
- analyzeFinal2(p, new_confl, conflict);
- return l_False;
- }
- }
- }
+ // if the uip was an assumption we are unsat
+ if (level(var(p)) <= assumptions.size())
+ {
+ for (int i = 0; i < learnt_clause.size(); ++i)
+ {
+ Assert(level(var(learnt_clause[i])) <= decisionLevel());
+ seen[var(learnt_clause[i])] = 1;
+ }
- cancelUntil(backtrack_level);
- uncheckedEnqueue(p, cr);
-
- varDecayActivity();
- claDecayActivity();
-
- if (--learntsize_adjust_cnt == 0){
- learntsize_adjust_confl *= learntsize_adjust_inc;
- learntsize_adjust_cnt = (int)learntsize_adjust_confl;
- max_learnts *= learntsize_inc;
-
- if (verbosity >= 1)
- printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
- (int)conflicts,
- (int)dec_vars
- - (trail_lim.size() == 0 ? trail.size()
- : trail_lim[0]),
- nClauses(),
- (int)clauses_literals,
- (int)max_learnts,
- nLearnts(),
- (double)learnts_literals / nLearnts(),
- progressEstimate() * 100);
- }
+ analyzeFinal(p, conflict);
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " conflict on assumptions " << std::endl;
+ return l_False;
+ }
- }else{
- // NO CONFLICT
- bool isWithinBudget;
- try {
- isWithinBudget =
- withinBudget(ResourceManager::Resource::BvSatConflictsStep);
- }
- catch (const CVC4::theory::Interrupted& e) {
- // do some clean-up and rethrow
- cancelUntil(assumptions.size());
- throw e;
- }
+ if (!CVC4::options::bvEagerExplanations())
+ {
+ // check if uip leads to a conflict
+ if (backtrack_level < assumptions.size())
+ {
+ cancelUntil(assumptions.size());
+ uncheckedEnqueue(p, cr);
- if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
- && conflictC >= nof_conflicts)
- || !isWithinBudget)
- {
- // Reached bound on number of conflicts:
- Debug("bvminisat::search")
- << OUTPUT_TAG << " restarting " << std::endl;
- progress_estimate = progressEstimate();
- cancelUntil(assumptions.size());
- return l_Undef;
- }
+ CRef new_confl = propagate();
+ if (new_confl != CRef_Undef)
+ {
+ // we have a conflict we now need to explain it
+ analyzeFinal2(p, new_confl, conflict);
+ return l_False;
+ }
+ }
+ }
- // Simplify the set of problem clauses:
- if (decisionLevel() == 0 && !simplify()) {
- Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
- return l_False;
- }
+ cancelUntil(backtrack_level);
+ uncheckedEnqueue(p, cr);
- // We can't erase clauses if there is unprocessed assumptions, there might be some
- // propagationg we need to redu
- if (decisionLevel() >= assumptions.size() && learnts.size()-nAssigns() >= max_learnts) {
- // Reduce the set of learnt clauses:
- Debug("bvminisat::search") << OUTPUT_TAG << " cleaning up database" << std::endl;
- reduceDB();
- }
+ varDecayActivity();
+ claDecayActivity();
- Lit next = lit_Undef;
- while (decisionLevel() < assumptions.size()){
- // Perform user provided assumption:
- Lit p = assumptions[decisionLevel()];
- if (value(p) == l_True){
- // Dummy decision level:
- newDecisionLevel();
- }else if (value(p) == l_False){
- marker[var(p)] = 2;
-
- analyzeFinal(~p, conflict);
- Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
- return l_False;
- }else{
- marker[var(p)] = 2;
- next = p;
- break;
- }
- }
+ if (--learntsize_adjust_cnt == 0)
+ {
+ learntsize_adjust_confl *= learntsize_adjust_inc;
+ learntsize_adjust_cnt = (int)learntsize_adjust_confl;
+ max_learnts *= learntsize_inc;
+
+ if (verbosity >= 1)
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+ (int)conflicts,
+ (int)dec_vars
+ - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]),
+ nClauses(),
+ (int)clauses_literals,
+ (int)max_learnts,
+ nLearnts(),
+ (double)learnts_literals / nLearnts(),
+ progressEstimate() * 100);
+ }
+ }
+ else
+ {
+ // NO CONFLICT
+ bool isWithinBudget;
+ try
+ {
+ isWithinBudget =
+ withinBudget(ResourceManager::Resource::BvSatConflictsStep);
+ }
+ catch (const CVC4::theory::Interrupted& e)
+ {
+ // do some clean-up and rethrow
+ cancelUntil(assumptions.size());
+ throw e;
+ }
- if (next == lit_Undef){
+ if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
+ && conflictC >= nof_conflicts)
+ || !isWithinBudget)
+ {
+ // Reached bound on number of conflicts:
+ Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
+ progress_estimate = progressEstimate();
+ cancelUntil(assumptions.size());
+ return l_Undef;
+ }
- if (only_bcp) {
- Debug("bvminisat::search") << OUTPUT_TAG << " only bcp, skipping rest of the problem" << std::endl;
- return l_True;
- }
+ // Simplify the set of problem clauses:
+ if (decisionLevel() == 0 && !simplify())
+ {
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
+ return l_False;
+ }
- // New variable decision:
- decisions++;
- next = pickBranchLit();
+ // We can't erase clauses if there is unprocessed assumptions, there might
+ // be some propagationg we need to redu
+ if (decisionLevel() >= assumptions.size()
+ && learnts.size() - nAssigns() >= max_learnts)
+ {
+ // Reduce the set of learnt clauses:
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " cleaning up database" << std::endl;
+ reduceDB();
+ }
- if (next == lit_Undef) {
- Debug("bvminisat::search") << OUTPUT_TAG << " satisfiable" << std::endl;
- // Model found:
- return l_True;
- }
- }
+ Lit next = lit_Undef;
+ while (decisionLevel() < assumptions.size())
+ {
+ // Perform user provided assumption:
+ Lit p = assumptions[decisionLevel()];
+ if (value(p) == l_True)
+ {
+ // Dummy decision level:
+ newDecisionLevel();
+ }
+ else if (value(p) == l_False)
+ {
+ marker[var(p)] = 2;
- // Increase decision level and enqueue 'next'
- newDecisionLevel();
- uncheckedEnqueue(next);
+ analyzeFinal(~p, conflict);
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
+ return l_False;
}
+ else
+ {
+ marker[var(p)] = 2;
+ next = p;
+ break;
+ }
+ }
+
+ if (next == lit_Undef)
+ {
+ if (only_bcp)
+ {
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " only bcp, skipping rest of the problem"
+ << std::endl;
+ return l_True;
+ }
+
+ // New variable decision:
+ decisions++;
+ next = pickBranchLit();
+
+ if (next == lit_Undef)
+ {
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " satisfiable" << std::endl;
+ // Model found:
+ return l_True;
+ }
+ }
+
+ // Increase decision level and enqueue 'next'
+ newDecisionLevel();
+ uncheckedEnqueue(next);
}
+ }
}
if (seen[x]) {
if (reason(x) == CRef_Undef) {
if (marker[x] == 2) {
- assert(level(x) > 0);
+ Assert(level(x) > 0);
explanation.push_back(trail[i]);
} else {
Assert(level(x) == 0);
fprintf(f, "p cnf %d %d\n", max, cnt);
for (int i = 0; i < assumps.size(); i++){
- assert(value(assumps[i]) != l_False);
- fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
+ Assert(value(assumps[i]) != l_False);
+ fprintf(f,
+ "%s%d 0\n",
+ sign(assumps[i]) ? "-" : "",
+ mapVar(var(assumps[i]), map, max) + 1);
}
for (int i = 0; i < clauses.size(); i++)
#include <vector>
+#include "base/check.h"
#include "context/context.h"
#include "proof/clause_id.h"
#include "prop/bvminisat/core/SolverTypes.h"
//=================================================================================================
// Implementation of inline methods:
-inline CRef Solver::reason(Var x) const { assert(x < vardata.size()); return vardata[x].reason; }
-inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; }
+inline CRef Solver::reason(Var x) const
+{
+ Assert(x < vardata.size());
+ return vardata[x].reason;
+}
+inline int Solver::level(Var x) const
+{
+ Assert(x < vardata.size());
+ return vardata[x].level;
+}
inline void Solver::insertVarOrder(Var x) {
if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
#ifndef BVMinisat_SolverTypes_h
#define BVMinisat_SolverTypes_h
-#include <assert.h>
-
-#include "prop/bvminisat/mtl/IntTypes.h"
+#include "base/check.h"
#include "prop/bvminisat/mtl/Alg.h"
-#include "prop/bvminisat/mtl/Vec.h"
-#include "prop/bvminisat/mtl/Map.h"
#include "prop/bvminisat/mtl/Alloc.h"
+#include "prop/bvminisat/mtl/IntTypes.h"
+#include "prop/bvminisat/mtl/Map.h"
+#include "prop/bvminisat/mtl/Vec.h"
namespace CVC4 {
namespace BVMinisat {
public:
void calcAbstraction() {
- assert(header.has_extra);
- uint32_t abstraction = 0;
- for (int i = 0; i < size(); i++)
- abstraction |= 1 << (var(data[i].lit) & 31);
- data[header.size].abs = abstraction; }
-
+ Assert(header.has_extra);
+ uint32_t abstraction = 0;
+ for (int i = 0; i < size(); i++)
+ abstraction |= 1 << (var(data[i].lit) & 31);
+ data[header.size].abs = abstraction;
+ }
int size () const { return header.size; }
- void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
+ void shrink(int i)
+ {
+ Assert(i <= size());
+ if (header.has_extra) data[header.size - i] = data[header.size];
+ header.size -= i;
+ }
void pop () { shrink(1); }
bool learnt () const { return header.learnt; }
bool has_extra () const { return header.has_extra; }
Lit operator [] (int i) const { return data[i].lit; }
operator const Lit* (void) const { return (Lit*)data; }
- float& activity () { assert(header.has_extra); return data[header.size].act; }
- uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
+ float& activity()
+ {
+ Assert(header.has_extra);
+ return data[header.size].act;
+ }
+ uint32_t abstraction() const
+ {
+ Assert(header.has_extra);
+ return data[header.size].abs;
+ }
Lit subsumes (const Clause& other) const;
void strengthen (Lit p);
template<class Lits>
CRef alloc(const Lits& ps, bool learnt = false)
{
- assert(sizeof(Lit) == sizeof(uint32_t));
- assert(sizeof(float) == sizeof(uint32_t));
- bool use_extra = learnt | extra_clause_field;
+ Assert(sizeof(Lit) == sizeof(uint32_t));
+ Assert(sizeof(float) == sizeof(uint32_t));
+ bool use_extra = learnt | extra_clause_field;
- CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
- new (lea(cid)) Clause(ps, use_extra, learnt);
+ CRef cid = RegionAllocator<uint32_t>::alloc(
+ clauseWord32Size(ps.size(), use_extra));
+ new (lea(cid)) Clause(ps, use_extra, learnt);
- return cid;
+ return cid;
}
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
{
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
- assert(!header.learnt); assert(!other.header.learnt);
- assert(header.has_extra); assert(other.header.has_extra);
+ Assert(!header.learnt);
+ Assert(!other.header.learnt);
+ Assert(header.has_extra);
+ Assert(other.header.has_extra);
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
return lit_Error;
#ifndef BVMinisat_Alg_h
#define BVMinisat_Alg_h
+#include "base/check.h"
#include "prop/bvminisat/mtl/Vec.h"
namespace CVC4 {
{
int j = 0;
for (; j < ts.size() && ts[j] != t; j++);
- assert(j < ts.size());
+ Assert(j < ts.size());
for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
ts.pop();
}
#ifndef BVMinisat_Alloc_h
#define BVMinisat_Alloc_h
-#include "prop/bvminisat/mtl/XAlloc.h"
+#include "base/check.h"
#include "prop/bvminisat/mtl/Vec.h"
+#include "prop/bvminisat/mtl/XAlloc.h"
namespace CVC4 {
namespace BVMinisat {
void free (int size) { wasted_ += size; }
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
- T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; }
- const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+ T& operator[](Ref r)
+ {
+ Assert(r >= 0 && r < sz);
+ return memory[r];
+ }
+ const T& operator[](Ref r) const
+ {
+ Assert(r >= 0 && r < sz);
+ return memory[r];
+ }
- T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; }
- const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
- Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
- return (Ref)(t - &memory[0]); }
+ T* lea(Ref r)
+ {
+ Assert(r >= 0 && r < sz);
+ return &memory[r];
+ }
+ const T* lea(Ref r) const
+ {
+ Assert(r >= 0 && r < sz);
+ return &memory[r];
+ }
+ Ref ael(const T* t)
+ {
+ Assert((void*)t >= (void*)&memory[0]
+ && (void*)t < (void*)&memory[sz - 1]);
+ return (Ref)(t - &memory[0]);
+ }
void moveTo(RegionAllocator& to) {
if (to.memory != NULL) ::free(to.memory);
}
// printf(" .. (%p) cap = %u\n", this, cap);
- assert(cap > 0);
+ Assert(cap > 0);
memory = (T*)xrealloc(memory, sizeof(T)*cap);
}
RegionAllocator<T>::alloc(int size)
{
// printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
- assert(size > 0);
+ Assert(size > 0);
capacity(sz + size);
uint32_t prev_sz = sz;
#ifndef BVMinisat_Heap_h
#define BVMinisat_Heap_h
+#include "base/check.h"
#include "prop/bvminisat/mtl/Vec.h"
namespace CVC4 {
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
- int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
-
-
- void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
- void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+ int operator[](int index) const
+ {
+ Assert(index < heap.size());
+ return heap[index];
+ }
+ void decrease(int n)
+ {
+ Assert(inHeap(n));
+ percolateUp(indices[n]);
+ }
+ void increase(int n)
+ {
+ Assert(inHeap(n));
+ percolateDown(indices[n]);
+ }
// Safe variant of insert/decrease/increase:
void update(int n)
void insert(int n)
{
indices.growTo(n+1, -1);
- assert(!inHeap(n));
+ Assert(!inHeap(n));
indices[n] = heap.size();
heap.push(n);
#ifndef BVMinisat_Map_h
#define BVMinisat_Map_h
+#include "base/check.h"
#include "prop/bvminisat/mtl/IntTypes.h"
#include "prop/bvminisat/mtl/Vec.h"
int size;
// Don't allow copying (error prone):
- Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
- Map (Map<K,D,H,E>& other) { assert(0); }
+ Map<K, D, H, E>& operator=(Map<K, D, H, E>& other) { Assert(0); }
+ Map(Map<K, D, H, E>& other) { Assert(0); }
bool checkCap(int new_size) const { return new_size > cap; }
// PRECONDITION: the key must already exist in the map.
const D& operator [] (const K& k) const
{
- assert(size != 0);
- const D* res = NULL;
- const vec<Pair>& ps = table[index(k)];
- for (int i = 0; i < ps.size(); i++)
- if (equals(ps[i].key, k))
- res = &ps[i].data;
- assert(res != NULL);
- return *res;
+ Assert(size != 0);
+ const D* res = NULL;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k)) res = &ps[i].data;
+ Assert(res != NULL);
+ return *res;
}
// PRECONDITION: the key must already exist in the map.
D& operator [] (const K& k)
{
- assert(size != 0);
- D* res = NULL;
- vec<Pair>& ps = table[index(k)];
- for (int i = 0; i < ps.size(); i++)
- if (equals(ps[i].key, k))
- res = &ps[i].data;
- assert(res != NULL);
- return *res;
+ Assert(size != 0);
+ D* res = NULL;
+ vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k)) res = &ps[i].data;
+ Assert(res != NULL);
+ return *res;
}
// PRECONDITION: the key must *NOT* exist in the map.
// PRECONDITION: the key must exist in the map.
void remove(const K& k) {
- assert(table != NULL);
- vec<Pair>& ps = table[index(k)];
- int j = 0;
- for (; j < ps.size() && !equals(ps[j].key, k); j++);
- assert(j < ps.size());
- ps[j] = ps.last();
- ps.pop();
- size--;
+ Assert(table != NULL);
+ vec<Pair>& ps = table[index(k)];
+ int j = 0;
+ for (; j < ps.size() && !equals(ps[j].key, k); j++)
+ ;
+ Assert(j < ps.size());
+ ps[j] = ps.last();
+ ps.pop();
+ size--;
}
void clear () {
#ifndef BVMinisat_Queue_h
#define BVMinisat_Queue_h
+#include "base/check.h"
#include "prop/bvminisat/mtl/Vec.h"
namespace CVC4 {
void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
- const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
- T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+ const T& operator[](int index) const
+ {
+ Assert(index >= 0);
+ Assert(index < size());
+ return buf[(first + index) % buf.size()];
+ }
+ T& operator[](int index)
+ {
+ Assert(index >= 0);
+ Assert(index < size());
+ return buf[(first + index) % buf.size()];
+ }
- T peek () const { assert(first != end); return buf[first]; }
- void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+ T peek() const
+ {
+ Assert(first != end);
+ return buf[first];
+ }
+ void pop()
+ {
+ Assert(first != end);
+ first++;
+ if (first == buf.size()) first = 0;
+ }
void insert(T elem) { // INVARIANT: buf[end] is always unused
buf[end++] = elem;
if (end == buf.size()) end = 0;
#ifndef BVMinisat_Vec_h
#define BVMinisat_Vec_h
-#include <assert.h>
#include <new>
+#include "base/check.h"
#include "prop/bvminisat/mtl/IntTypes.h"
#include "prop/bvminisat/mtl/XAlloc.h"
int cap;
// Don't allow copying (error prone):
- vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
- vec (vec<T>& other) { assert(0); }
-
+ vec<T>& operator=(vec<T>& other)
+ {
+ Assert(0);
+ return *this;
+ }
+ vec(vec<T>& other) { Assert(0); }
+
// Helpers for calculating next capacity:
static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
//static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
// Size operations:
int size (void) const { return sz; }
- void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
- void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
+ void shrink(int nelems)
+ {
+ Assert(nelems <= sz);
+ for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
+ }
+ void shrink_(int nelems)
+ {
+ Assert(nelems <= sz);
+ sz -= nelems;
+ }
int capacity (void) const { return cap; }
void capacity (int min_cap);
void growTo (int size);
// Stack interface:
void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
- void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
- void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ void push_(const T& elem)
+ {
+ Assert(sz < cap);
+ data[sz++] = elem;
+ }
+ void pop(void)
+ {
+ Assert(sz > 0);
+ sz--, data[sz].~T();
+ }
// NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
// in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
// happen given the way capacities are calculated (below). Essentially, all capacities are
#include "prop/bvminisat/simp/SimpSolver.h"
+#include "base/check.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
Var v = var(assumptions[i]);
// If an assumption has been eliminated, remember it.
- assert(!isEliminated(v));
+ Assert(!isEliminated(v));
if (!frozen[v]){
// Freeze and store.
bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
{
#ifndef NDEBUG
- for (int i = 0; i < ps.size(); i++)
- assert(!isEliminated(var(ps[i])));
+ for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
#endif
int nclauses = clauses.size();
bool SimpSolver::strengthenClause(CRef cr, Lit l)
{
Clause& clause = ca[cr];
- assert(decisionLevel() == 0);
- assert(use_simplification);
+ Assert(decisionLevel() == 0);
+ Assert(use_simplification);
// FIX: this is too inefficient but would be nice to have (properly
// implemented) if (!find(subsumption_queue, &clause))
bool SimpSolver::implied(const vec<Lit>& clause)
{
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
- trail_lim.push(trail.size());
- for (int i = 0; i < clause.size(); i++)
- if (value(clause[i]) == l_True)
- {
- cancelUntil(0);
- return false;
- }
- else if (value(clause[i]) != l_False)
- {
- assert(value(clause[i]) == l_Undef);
- uncheckedEnqueue(~clause[i]);
- }
+ trail_lim.push(trail.size());
+ for (int i = 0; i < clause.size(); i++)
+ {
+ if (value(clause[i]) == l_True)
+ {
+ cancelUntil(0);
+ return false;
+ }
+ else if (value(clause[i]) != l_False)
+ {
+ Assert(value(clause[i]) == l_Undef);
+ uncheckedEnqueue(~clause[i]);
+ }
+ }
- bool result = propagate() != CRef_Undef;
- cancelUntil(0);
- return result;
+ bool result = propagate() != CRef_Undef;
+ cancelUntil(0);
+ return result;
}
int cnt = 0;
int subsumed = 0;
int deleted_literals = 0;
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
- assert(clause.size() > 1
+ Assert(clause.size() > 1
|| value(clause[0]) == l_True); // Unit-clauses should have been
// propagated before this point.
bool SimpSolver::asymm(Var v, CRef cr)
{
Clause& clause = ca[cr];
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
if (clause.mark() || satisfied(clause)) return true;
bool SimpSolver::asymmVar(Var v)
{
- assert(use_simplification);
+ Assert(use_simplification);
- const vec<CRef>& cls = occurs.lookup(v);
+ const vec<CRef>& cls = occurs.lookup(v);
- if (value(v) != l_Undef || cls.size() == 0)
- return true;
+ if (value(v) != l_Undef || cls.size() == 0) return true;
- for (int i = 0; i < cls.size(); i++)
- if (!asymm(v, cls[i]))
- return false;
+ for (int i = 0; i < cls.size(); i++)
+ if (!asymm(v, cls[i])) return false;
- return backwardSubsumptionCheck();
+ return backwardSubsumptionCheck();
}
elimclauses.push(toInt(clause[i]));
if (var(clause[i]) == v) v_pos = i + first;
}
- assert(v_pos != -1);
+ Assert(v_pos != -1);
// Swap the first literal with the 'v' literal, so that the literal
// containing 'v' will occur first in the clause:
bool SimpSolver::eliminateVar(Var v)
{
+ Assert(!frozen[v]);
+ Assert(!isEliminated(v));
+ Assert(value(v) == l_Undef);
+
+ // Split the occurrences into positive and negative:
+ //
+ const vec<CRef>& cls = occurs.lookup(v);
+ vec<CRef> pos, neg;
+ for (int i = 0; i < cls.size(); i++)
+ (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+ // Check whether the increase in number of clauses stays within the allowed
+ // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
+ // size (if it is set):
+ //
+ int cnt = 0;
+ int clause_size = 0;
+
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+ && (++cnt > cls.size() + grow
+ || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
- assert(!frozen[v]);
- assert(!isEliminated(v));
- assert(value(v) == l_Undef);
-
- // Split the occurrences into positive and negative:
- //
- const vec<CRef>& cls = occurs.lookup(v);
- vec<CRef> pos, neg;
- for (int i = 0; i < cls.size(); i++)
- (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
-
- // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
- // clause must exceed the limit on the maximal clause size (if it is set):
- //
- int cnt = 0;
- int clause_size = 0;
+ // Delete and store old clauses:
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ eliminated_vars++;
+ if (pos.size() > neg.size())
+ {
+ for (int i = 0; i < neg.size(); i++)
+ mkElimClause(elimclauses, v, ca[neg[i]]);
+ mkElimClause(elimclauses, mkLit(v));
+ }
+ else
+ {
for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
- && (++cnt > cls.size() + grow
- || (clause_lim != -1 && clause_size > clause_lim)))
- return true;
-
- // Delete and store old clauses:
- eliminated[v] = true;
- setDecisionVar(v, false);
- eliminated_vars++;
-
- if (pos.size() > neg.size()){
- for (int i = 0; i < neg.size(); i++)
- mkElimClause(elimclauses, v, ca[neg[i]]);
- mkElimClause(elimclauses, mkLit(v));
- }else{
- for (int i = 0; i < pos.size(); i++)
- mkElimClause(elimclauses, v, ca[pos[i]]);
- mkElimClause(elimclauses, ~mkLit(v));
- }
+ mkElimClause(elimclauses, v, ca[pos[i]]);
+ mkElimClause(elimclauses, ~mkLit(v));
+ }
for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
bool SimpSolver::substitute(Var v, Lit x)
{
- assert(!frozen[v]);
- assert(!isEliminated(v));
- assert(value(v) == l_Undef);
-
- if (!ok) return false;
+ Assert(!frozen[v]);
+ Assert(!isEliminated(v));
+ Assert(value(v) == l_Undef);
- eliminated[v] = true;
- setDecisionVar(v, false);
- const vec<CRef>& cls = occurs.lookup(v);
+ if (!ok) return false;
- vec<Lit>& subst_clause = add_tmp;
- for (int i = 0; i < cls.size(); i++){
- Clause& clause = ca[cls[i]];
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ const vec<CRef>& cls = occurs.lookup(v);
- subst_clause.clear();
- for (int j = 0; j < clause.size(); j++)
- {
- Lit p = clause[j];
- subst_clause.push(var(p) == v ? x ^ sign(p) : p);
- }
+ vec<Lit>& subst_clause = add_tmp;
+ for (int i = 0; i < cls.size(); i++)
+ {
+ Clause& clause = ca[cls[i]];
- removeClause(cls[i]);
- ClauseId id;
- if (!addClause_(subst_clause, id))
- return ok = false;
+ subst_clause.clear();
+ for (int j = 0; j < clause.size(); j++)
+ {
+ Lit p = clause[j];
+ subst_clause.push(var(p) == v ? x ^ sign(p) : p);
}
+ removeClause(cls[i]);
+ ClauseId id;
+ if (!addClause_(subst_clause, id)) return ok = false;
+ }
+
return true;
}
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
- assert(bwdsub_assigns == trail.size());
- assert(subsumption_queue.size() == 0);
- assert(n_touched == 0);
- elim_heap.clear();
- goto cleanup; }
+ Assert(bwdsub_assigns == trail.size());
+ Assert(subsumption_queue.size() == 0);
+ Assert(n_touched == 0);
+ elim_heap.clear();
+ goto cleanup;
+ }
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
checkGarbage(simp_garbage_frac);
}
- assert(subsumption_queue.size() == 0);
+ Assert(subsumption_queue.size() == 0);
}
cleanup:
#ifndef BVMinisat_SimpSolver_h
#define BVMinisat_SimpSolver_h
+#include "base/check.h"
#include "proof/clause_id.h"
#include "prop/bvminisat/core/Solver.h"
#include "prop/bvminisat/mtl/Queue.h"
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
inline void SimpSolver::updateElimHeap(Var v) {
- assert(use_simplification);
- // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
- if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
- elim_heap.update(v); }
-
+ Assert(use_simplification);
+ // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+ if (elim_heap.inHeap(v)
+ || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+ elim_heap.update(v);
+}
inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); }
inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); }
#include <iostream>
#include <unordered_set>
+#include "base/check.h"
#include "base/output.h"
#include "options/main_options.h"
#include "options/prop_options.h"
}
void Solver::resizeVars(int newSize) {
- assert(d_enable_incremental);
- assert(decisionLevel() == 0);
+ Assert(d_enable_incremental);
+ Assert(decisionLevel() == 0);
Assert(newSize >= 2) << "always keep true/false";
if (newSize < nVars()) {
int shrinkSize = nVars() - newSize;
if (Debug.isOn("minisat::pop")) {
for (int i = 0; i < trail.size(); ++ i) {
- assert(var(trail[i]) < nVars());
+ Assert(var(trail[i]) < nVars());
}
}
}
id = ClauseIdUndef;
}
} else {
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
// Check if it propagates
if (ps.size() == falseLiteralsCount + 1) {
if(assigns[var(ps[0])] == l_Undef) {
- assert(assigns[var(ps[0])] != l_False);
+ Assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
Debug("cores") << "i'm registering a unit clause, maybe input"
<< std::endl;
Debug("minisat") << "\n";
}
- assert(c.size() > 1);
+ Assert(c.size() > 1);
if (options::unsatCores() && !isProofEnabled())
{
ProofManager::getSatProof()->markDeleted(cr);
d_pfManager->startResChain(ca[confl]);
}
do{
- assert(confl != CRef_Undef); // (otherwise should be UIP)
+ Assert(confl != CRef_Undef); // (otherwise should be UIP)
- {
- // ! IMPORTANT !
- // It is not safe to use c after this block of code because
- // resolveOutUnit() below may lead to clauses being allocated, which
- // in turn may lead to reallocations that invalidate c.
- Clause& c = ca[confl];
- max_resolution_level = std::max(max_resolution_level, c.level());
-
- if (c.removable()) claBumpActivity(c);
- }
+ {
+ // ! IMPORTANT !
+ // It is not safe to use c after this block of code because
+ // resolveOutUnit() below may lead to clauses being allocated, which
+ // in turn may lead to reallocations that invalidate c.
+ Clause& c = ca[confl];
+ max_resolution_level = std::max(max_resolution_level, c.level());
+
+ if (c.removable()) claBumpActivity(c);
+ }
if (Trace.isOn("pf::sat"))
{
int top = analyze_toclear.size();
while (analyze_stack.size() > 0){
CRef c_reason = reason(var(analyze_stack.last()));
- assert(c_reason != CRef_Undef);
+ Assert(c_reason != CRef_Undef);
Clause& c = ca[c_reason];
int c_size = c.size();
analyze_stack.pop();
Var x = var(trail[i]);
if (seen[x]){
if (reason(x) == CRef_Undef){
- assert(level(x) > 0);
- out_conflict.push(~trail[i]);
+ Assert(level(x) > 0);
+ out_conflict.push(~trail[i]);
}else{
Clause& c = ca[reason(x)];
for (int j = 1; j < c.size(); j++)
}
Debug("minisat") << "\n";
}
- assert(value(p) == l_Undef);
- assert(var(p) < nVars());
+ Assert(value(p) == l_Undef);
+ Assert(var(p) < nVars());
assigns[var(p)] = lbool(!sign(p));
vardata[var(p)] = VarData(
from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
Lit false_lit = ~p;
if (c[0] == false_lit)
c[0] = c[1], c[1] = false_lit;
- assert(c[1] == false_lit);
+ Assert(c[1] == false_lit);
i++;
// If 0th watch is true, then clause is already satisfied.
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (c.level() > level) {
- assert(!locked(c));
- removeClause(cs[i]);
+ Assert(!locked(c));
+ removeClause(cs[i]);
} else {
cs[j++] = cs[i];
}
|________________________________________________________________________________________________@*/
bool Solver::simplify()
{
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
- if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef)
- return ok = false;
+ if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false;
- if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
- return true;
+ if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
- // Remove satisfied clauses:
- removeSatisfied(clauses_removable);
- if (remove_satisfied) // Can be turned off.
- removeSatisfied(clauses_persistent);
- checkGarbage();
- rebuildOrderHeap();
+ // Remove satisfied clauses:
+ removeSatisfied(clauses_removable);
+ if (remove_satisfied) // Can be turned off.
+ removeSatisfied(clauses_persistent);
+ checkGarbage();
+ rebuildOrderHeap();
- simpDB_assigns = nAssigns();
- simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
+ simpDB_assigns = nAssigns();
+ simpDB_props =
+ clauses_literals + learnts_literals; // (shouldn't depend on stats
+ // really, but it will do for now)
- return true;
+ return true;
}
|________________________________________________________________________________________________@*/
lbool Solver::search(int nof_conflicts)
{
- assert(ok);
- int backtrack_level;
- int conflictC = 0;
- vec<Lit> learnt_clause;
- starts++;
-
- TheoryCheckType check_type = CHECK_WITH_THEORY;
- for (;;) {
-
- // Propagate and call the theory solvers
- CRef confl = propagate(check_type);
- Assert(lemmas.size() == 0);
-
- if (confl != CRef_Undef) {
+ Assert(ok);
+ int backtrack_level;
+ int conflictC = 0;
+ vec<Lit> learnt_clause;
+ starts++;
+
+ TheoryCheckType check_type = CHECK_WITH_THEORY;
+ for (;;)
+ {
+ // Propagate and call the theory solvers
+ CRef confl = propagate(check_type);
+ Assert(lemmas.size() == 0);
- conflicts++; conflictC++;
+ if (confl != CRef_Undef)
+ {
+ conflicts++;
+ conflictC++;
- if (decisionLevel() == 0)
- {
- if (options::unsatCores() && !isProofEnabled())
- {
- ProofManager::getSatProof()->finalizeProof(confl);
- }
- if (isProofEnabled())
- {
- if (confl == CRef_Lazy)
- {
- d_pfManager->finalizeProof();
- }
- else
- {
- d_pfManager->finalizeProof(ca[confl]);
- }
- }
- return l_False;
- }
+ if (decisionLevel() == 0)
+ {
+ if (options::unsatCores() && !isProofEnabled())
+ {
+ ProofManager::getSatProof()->finalizeProof(confl);
+ }
+ if (isProofEnabled())
+ {
+ if (confl == CRef_Lazy)
+ {
+ d_pfManager->finalizeProof();
+ }
+ else
+ {
+ d_pfManager->finalizeProof(ca[confl]);
+ }
+ }
+ return l_False;
+ }
- // Analyze the conflict
- learnt_clause.clear();
- int max_level = analyze(confl, learnt_clause, backtrack_level);
- cancelUntil(backtrack_level);
+ // Analyze the conflict
+ learnt_clause.clear();
+ int max_level = analyze(confl, learnt_clause, backtrack_level);
+ cancelUntil(backtrack_level);
- // Assert the conflict clause and the asserting literal
- if (learnt_clause.size() == 1) {
- uncheckedEnqueue(learnt_clause[0]);
- if (options::unsatCores() && !isProofEnabled())
- {
- ProofManager::getSatProof()->endResChain(learnt_clause[0]);
- }
- if (isProofEnabled())
- {
- d_pfManager->endResChain(learnt_clause[0]);
- }
- } else {
- CRef cr =
- ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
+ // Assert the conflict clause and the asserting literal
+ if (learnt_clause.size() == 1)
+ {
+ uncheckedEnqueue(learnt_clause[0]);
+ if (options::unsatCores() && !isProofEnabled())
+ {
+ ProofManager::getSatProof()->endResChain(learnt_clause[0]);
+ }
+ if (isProofEnabled())
+ {
+ d_pfManager->endResChain(learnt_clause[0]);
+ }
+ }
+ else
+ {
+ CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
learnt_clause,
true);
- clauses_removable.push(cr);
- attachClause(cr);
- claBumpActivity(ca[cr]);
- uncheckedEnqueue(learnt_clause[0], cr);
- if (options::unsatCores() && !isProofEnabled())
- {
- ClauseId id =
- ProofManager::getSatProof()->registerClause(cr, LEARNT);
- ProofManager::getSatProof()->endResChain(id);
- }
- if (isProofEnabled())
- {
- d_pfManager->endResChain(ca[cr]);
- }
- }
-
- varDecayActivity();
- claDecayActivity();
-
- if (--learntsize_adjust_cnt == 0){
- learntsize_adjust_confl *= learntsize_adjust_inc;
- learntsize_adjust_cnt = (int)learntsize_adjust_confl;
- max_learnts *= learntsize_inc;
-
- if (verbosity >= 1)
- printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
- (int)conflicts,
- (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
- (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
- }
+ clauses_removable.push(cr);
+ attachClause(cr);
+ claBumpActivity(ca[cr]);
+ uncheckedEnqueue(learnt_clause[0], cr);
+ if (options::unsatCores() && !isProofEnabled())
+ {
+ ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
+ ProofManager::getSatProof()->endResChain(id);
+ }
+ if (isProofEnabled())
+ {
+ d_pfManager->endResChain(ca[cr]);
+ }
+ }
- if (theoryConflict && options::sat_refine_conflicts()) {
- check_type = CHECK_FINAL_FAKE;
- } else {
- check_type = CHECK_WITH_THEORY;
- }
+ varDecayActivity();
+ claDecayActivity();
- } else {
- // If this was a final check, we are satisfiable
- if (check_type == CHECK_FINAL)
- {
- bool decisionEngineDone = d_proxy->isDecisionEngineDone();
- // Unless a lemma has added more stuff to the queues
- if (!decisionEngineDone
- && (!order_heap.empty() || qhead < trail.size()))
- {
- check_type = CHECK_WITH_THEORY;
- continue;
- }
- else if (recheck)
- {
- // There some additional stuff added, so we go for another
- // full-check
- continue;
- }
- else
- {
- // Yes, we're truly satisfiable
- return l_True;
- }
- }
- else if (check_type == CHECK_FINAL_FAKE)
- {
- check_type = CHECK_WITH_THEORY;
- }
+ if (--learntsize_adjust_cnt == 0)
+ {
+ learntsize_adjust_confl *= learntsize_adjust_inc;
+ learntsize_adjust_cnt = (int)learntsize_adjust_confl;
+ max_learnts *= learntsize_inc;
+
+ if (verbosity >= 1)
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+ (int)conflicts,
+ (int)dec_vars
+ - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]),
+ nClauses(),
+ (int)clauses_literals,
+ (int)max_learnts,
+ nLearnts(),
+ (double)learnts_literals / nLearnts(),
+ progressEstimate() * 100);
+ }
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
- || !withinBudget(ResourceManager::Resource::SatConflictStep))
- {
- // Reached bound on number of conflicts:
- progress_estimate = progressEstimate();
- cancelUntil(0);
- // [mdeters] notify theory engine of restarts for deferred
- // theory processing
- d_proxy->notifyRestart();
- return l_Undef;
- }
+ if (theoryConflict && options::sat_refine_conflicts())
+ {
+ check_type = CHECK_FINAL_FAKE;
+ }
+ else
+ {
+ check_type = CHECK_WITH_THEORY;
+ }
+ }
+ else
+ {
+ // If this was a final check, we are satisfiable
+ if (check_type == CHECK_FINAL)
+ {
+ bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+ // Unless a lemma has added more stuff to the queues
+ if (!decisionEngineDone
+ && (!order_heap.empty() || qhead < trail.size()))
+ {
+ check_type = CHECK_WITH_THEORY;
+ continue;
+ }
+ else if (recheck)
+ {
+ // There some additional stuff added, so we go for another
+ // full-check
+ continue;
+ }
+ else
+ {
+ // Yes, we're truly satisfiable
+ return l_True;
+ }
+ }
+ else if (check_type == CHECK_FINAL_FAKE)
+ {
+ check_type = CHECK_WITH_THEORY;
+ }
- // Simplify the set of problem clauses:
- if (decisionLevel() == 0 && !simplify()) {
- return l_False;
- }
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+ || !withinBudget(ResourceManager::Resource::SatConflictStep))
+ {
+ // Reached bound on number of conflicts:
+ progress_estimate = progressEstimate();
+ cancelUntil(0);
+ // [mdeters] notify theory engine of restarts for deferred
+ // theory processing
+ d_proxy->notifyRestart();
+ return l_Undef;
+ }
- if (clauses_removable.size()-nAssigns() >= max_learnts) {
- // Reduce the set of learnt clauses:
- reduceDB();
- }
+ // Simplify the set of problem clauses:
+ if (decisionLevel() == 0 && !simplify())
+ {
+ return l_False;
+ }
- Lit next = lit_Undef;
- while (decisionLevel() < assumptions.size()) {
- // Perform user provided assumption:
- Lit p = assumptions[decisionLevel()];
- if (value(p) == l_True) {
- // Dummy decision level:
- newDecisionLevel();
- } else if (value(p) == l_False) {
- analyzeFinal(~p, d_conflict);
- return l_False;
- } else {
- next = p;
- break;
- }
- }
+ if (clauses_removable.size() - nAssigns() >= max_learnts)
+ {
+ // Reduce the set of learnt clauses:
+ reduceDB();
+ }
- if (next == lit_Undef) {
- // New variable decision:
- next = pickBranchLit();
+ Lit next = lit_Undef;
+ while (decisionLevel() < assumptions.size())
+ {
+ // Perform user provided assumption:
+ Lit p = assumptions[decisionLevel()];
+ if (value(p) == l_True)
+ {
+ // Dummy decision level:
+ newDecisionLevel();
+ }
+ else if (value(p) == l_False)
+ {
+ analyzeFinal(~p, d_conflict);
+ return l_False;
+ }
+ else
+ {
+ next = p;
+ break;
+ }
+ }
- if (next == lit_Undef) {
- // We need to do a full theory check to confirm
- Debug("minisat::search") << "Doing a full theory check..."
- << std::endl;
- check_type = CHECK_FINAL;
- continue;
- }
- }
+ if (next == lit_Undef)
+ {
+ // New variable decision:
+ next = pickBranchLit();
- // Increase decision level and enqueue 'next'
- newDecisionLevel();
- uncheckedEnqueue(next);
+ if (next == lit_Undef)
+ {
+ // We need to do a full theory check to confirm
+ Debug("minisat::search")
+ << "Doing a full theory check..." << std::endl;
+ check_type = CHECK_FINAL;
+ continue;
}
+ }
+
+ // Increase decision level and enqueue 'next'
+ newDecisionLevel();
+ uncheckedEnqueue(next);
}
+ }
}
ScopedBool scoped_bool(minisat_busy, true);
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
model.clear();
d_conflict.clear();
fprintf(f, "p cnf %d %d\n", max, cnt);
for (int i = 0; i < assumptions.size(); i++){
- assert(value(assumptions[i]) != l_False);
- fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
+ Assert(value(assumptions[i]) != l_False);
+ fprintf(f,
+ "%s%d 0\n",
+ sign(assumptions[i]) ? "-" : "",
+ mapVar(var(assumptions[i]), map, max) + 1);
}
for (int i = 0; i < clauses_persistent.size(); i++)
void Solver::push()
{
- assert(d_enable_incremental);
- assert(decisionLevel() == 0);
+ Assert(d_enable_incremental);
+ Assert(decisionLevel() == 0);
++assertionLevel;
Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
void Solver::pop()
{
- assert(d_enable_incremental);
+ Assert(d_enable_incremental);
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
// Pop the trail below the user level
--assertionLevel;
#ifndef Minisat_Solver_h
#define Minisat_Solver_h
-#include "cvc4_private.h"
-
#include <iosfwd>
+#include "base/check.h"
#include "base/output.h"
#include "context/context.h"
+#include "cvc4_private.h"
#include "expr/proof_node_manager.h"
#include "proof/clause_id.h"
#include "prop/minisat/core/SolverTypes.h"
inline int Solver::level(Var x) const
{
- assert(x < vardata.size());
+ Assert(x < vardata.size());
return vardata[x].d_level;
}
inline int Solver::user_level(Var x) const
{
- assert(x < vardata.size());
+ Assert(x < vardata.size());
return vardata[x].d_user_level;
}
inline int Solver::intro_level(Var x) const
{
- assert(x < vardata.size());
+ Assert(x < vardata.size());
return vardata[x].d_intro_level;
}
inline int Solver::trail_index(Var x) const
{
- assert(x < vardata.size());
+ Assert(x < vardata.size());
return vardata[x].d_trail_index;
}
inline void Solver::insertVarOrder(Var x) {
- assert(x < vardata.size());
- if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
+ Assert(x < vardata.size());
+ if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
+}
inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
-inline lbool Solver::value (Var x) const { assert(x < nVars()); return assigns[x]; }
-inline lbool Solver::value (Lit p) const { assert(var(p) < nVars()); return assigns[var(p)] ^ sign(p); }
+inline lbool Solver::value(Var x) const
+{
+ Assert(x < nVars());
+ return assigns[x];
+}
+inline lbool Solver::value(Lit p) const
+{
+ Assert(var(p) < nVars());
+ return assigns[var(p)] ^ sign(p);
+}
inline lbool Solver::modelValue (Var x) const { return model[x]; }
inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
inline int Solver::nAssigns () const { return trail.size(); }
#ifndef Minisat_SolverTypes_h
#define Minisat_SolverTypes_h
-#include <assert.h>
+#include "base/check.h"
#include "base/output.h"
-#include "prop/minisat/mtl/IntTypes.h"
#include "prop/minisat/mtl/Alg.h"
-#include "prop/minisat/mtl/Vec.h"
-#include "prop/minisat/mtl/Map.h"
#include "prop/minisat/mtl/Alloc.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/Map.h"
+#include "prop/minisat/mtl/Vec.h"
namespace CVC4 {
namespace Minisat {
public:
void calcAbstraction() {
- assert(header.has_extra);
- uint32_t abstraction = 0;
- for (int i = 0; i < size(); i++)
- abstraction |= 1 << (var(data[i].lit) & 31);
- data[header.size].abs = abstraction; }
-
+ Assert(header.has_extra);
+ uint32_t abstraction = 0;
+ for (int i = 0; i < size(); i++)
+ abstraction |= 1 << (var(data[i].lit) & 31);
+ data[header.size].abs = abstraction;
+ }
int level () const { return header.level; }
int size () const { return header.size; }
- void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
+ void shrink(int i)
+ {
+ Assert(i <= size());
+ if (header.has_extra) data[header.size - i] = data[header.size];
+ header.size -= i;
+ }
void pop () { shrink(1); }
bool removable () const { return header.removable; }
bool has_extra () const { return header.has_extra; }
Lit operator [] (int i) const { return data[i].lit; }
operator const Lit* (void) const { return (Lit*)data; }
- float& activity () { assert(header.has_extra); return data[header.size].act; }
- uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
+ float& activity()
+ {
+ Assert(header.has_extra);
+ return data[header.size].act;
+ }
+ uint32_t abstraction() const
+ {
+ Assert(header.has_extra);
+ return data[header.size].abs;
+ }
Lit subsumes (const Clause& other) const;
void strengthen (Lit p);
template<class Lits>
CRef alloc(int level, const Lits& ps, bool removable = false)
{
- assert(sizeof(Lit) == sizeof(uint32_t));
- assert(sizeof(float) == sizeof(uint32_t));
- bool use_extra = removable | extra_clause_field;
+ Assert(sizeof(Lit) == sizeof(uint32_t));
+ Assert(sizeof(float) == sizeof(uint32_t));
+ bool use_extra = removable | extra_clause_field;
- CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
- new (lea(cid)) Clause(ps, use_extra, removable, level);
+ CRef cid = RegionAllocator<uint32_t>::alloc(
+ clauseWord32Size(ps.size(), use_extra));
+ new (lea(cid)) Clause(ps, use_extra, removable, level);
- return cid;
+ return cid;
}
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
- assert(!header.removable); assert(!other.header.removable);
- assert(header.has_extra); assert(other.header.has_extra);
+ Assert(!header.removable);
+ Assert(!other.header.removable);
+ Assert(header.has_extra);
+ Assert(other.header.has_extra);
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
return lit_Error;
#ifndef Minisat_Alg_h
#define Minisat_Alg_h
+#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
namespace CVC4 {
{
int j = 0;
for (; j < ts.size() && ts[j] != t; j++);
- assert(j < ts.size());
+ Assert(j < ts.size());
for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
ts.pop();
}
#ifndef Minisat_Alloc_h
#define Minisat_Alloc_h
-#include "prop/minisat/mtl/XAlloc.h"
+#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/mtl/XAlloc.h"
namespace CVC4 {
namespace Minisat {
void free (int size) { wasted_ += size; }
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
- T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; }
- const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+ T& operator[](Ref r)
+ {
+ Assert(r >= 0 && r < sz);
+ return memory[r];
+ }
+ const T& operator[](Ref r) const
+ {
+ Assert(r >= 0 && r < sz);
+ return memory[r];
+ }
- T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; }
- const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
- Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
- return (Ref)(t - &memory[0]); }
+ T* lea(Ref r)
+ {
+ Assert(r >= 0 && r < sz);
+ return &memory[r];
+ }
+ const T* lea(Ref r) const
+ {
+ Assert(r >= 0 && r < sz);
+ return &memory[r];
+ }
+ Ref ael(const T* t)
+ {
+ Assert((void*)t >= (void*)&memory[0]
+ && (void*)t < (void*)&memory[sz - 1]);
+ return (Ref)(t - &memory[0]);
+ }
void moveTo(RegionAllocator& to) {
if (to.memory != NULL) ::free(to.memory);
}
// printf(" .. (%p) cap = %u\n", this, cap);
- assert(cap > 0);
+ Assert(cap > 0);
memory = (T*)xrealloc(memory, sizeof(T)*cap);
}
RegionAllocator<T>::alloc(int size)
{
// printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
- assert(size > 0);
+ Assert(size > 0);
capacity(sz + size);
uint32_t prev_sz = sz;
#ifndef Minisat_Heap_h
#define Minisat_Heap_h
+#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
namespace CVC4 {
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
- int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
-
-
- void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
- void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+ int operator[](int index) const
+ {
+ Assert(index < heap.size());
+ return heap[index];
+ }
+ void decrease(int n)
+ {
+ Assert(inHeap(n));
+ percolateUp(indices[n]);
+ }
+ void increase(int n)
+ {
+ Assert(inHeap(n));
+ percolateDown(indices[n]);
+ }
// Safe variant of insert/decrease/increase:
void update(int n)
void insert(int n)
{
indices.growTo(n+1, -1);
- assert(!inHeap(n));
+ Assert(!inHeap(n));
indices[n] = heap.size();
heap.push(n);
#ifndef Minisat_Map_h
#define Minisat_Map_h
+#include "base/check.h"
#include "prop/minisat/mtl/IntTypes.h"
#include "prop/minisat/mtl/Vec.h"
int size;
// Don't allow copying (error prone):
- Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
- Map (Map<K,D,H,E>& other) { assert(0); }
+ Map<K, D, H, E>& operator=(Map<K, D, H, E>& other) { Assert(0); }
+ Map(Map<K, D, H, E>& other) { Assert(0); }
bool checkCap(int new_size) const { return new_size > cap; }
// PRECONDITION: the key must already exist in the map.
const D& operator [] (const K& k) const
{
- assert(size != 0);
- const D* res = NULL;
- const vec<Pair>& ps = table[index(k)];
- for (int i = 0; i < ps.size(); i++)
- if (equals(ps[i].key, k))
- res = &ps[i].data;
- assert(res != NULL);
- return *res;
+ Assert(size != 0);
+ const D* res = NULL;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k)) res = &ps[i].data;
+ Assert(res != NULL);
+ return *res;
}
// PRECONDITION: the key must already exist in the map.
D& operator [] (const K& k)
{
- assert(size != 0);
- D* res = NULL;
- vec<Pair>& ps = table[index(k)];
- for (int i = 0; i < ps.size(); i++)
- if (equals(ps[i].key, k))
- res = &ps[i].data;
- assert(res != NULL);
- return *res;
+ Assert(size != 0);
+ D* res = NULL;
+ vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k)) res = &ps[i].data;
+ Assert(res != NULL);
+ return *res;
}
// PRECONDITION: the key must *NOT* exist in the map.
// PRECONDITION: the key must exist in the map.
void remove(const K& k) {
- assert(table != NULL);
- vec<Pair>& ps = table[index(k)];
- int j = 0;
- for (; j < ps.size() && !equals(ps[j].key, k); j++);
- assert(j < ps.size());
- ps[j] = ps.last();
- ps.pop();
- size--;
+ Assert(table != NULL);
+ vec<Pair>& ps = table[index(k)];
+ int j = 0;
+ for (; j < ps.size() && !equals(ps[j].key, k); j++)
+ ;
+ Assert(j < ps.size());
+ ps[j] = ps.last();
+ ps.pop();
+ size--;
}
void clear () {
#ifndef Minisat_Queue_h
#define Minisat_Queue_h
+#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
namespace CVC4 {
void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
- const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
- T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+ const T& operator[](int index) const
+ {
+ Assert(index >= 0);
+ Assert(index < size());
+ return buf[(first + index) % buf.size()];
+ }
+ T& operator[](int index)
+ {
+ Assert(index >= 0);
+ Assert(index < size());
+ return buf[(first + index) % buf.size()];
+ }
- T peek () const { assert(first != end); return buf[first]; }
- void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+ T peek() const
+ {
+ Assert(first != end);
+ return buf[first];
+ }
+ void pop()
+ {
+ Assert(first != end);
+ first++;
+ if (first == buf.size()) first = 0;
+ }
void insert(T elem) { // INVARIANT: buf[end] is always unused
buf[end++] = elem;
if (end == buf.size()) end = 0;
#ifndef Minisat_Vec_h
#define Minisat_Vec_h
-#include <assert.h>
#include <new>
+#include "base/check.h"
#include "prop/minisat/mtl/IntTypes.h"
#include "prop/minisat/mtl/XAlloc.h"
int cap;
// Don't allow copying (error prone):
- vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
- vec (vec<T>& other) { assert(0); }
-
+ vec<T>& operator=(vec<T>& other)
+ {
+ Assert(0);
+ return *this;
+ }
+ vec(vec<T>& other) { Assert(0); }
+
// Helpers for calculating next capacity:
static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
//static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
// Size operations:
int size (void) const { return sz; }
- void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
- void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
+ void shrink(int nelems)
+ {
+ Assert(nelems <= sz);
+ for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
+ }
+ void shrink_(int nelems)
+ {
+ Assert(nelems <= sz);
+ sz -= nelems;
+ }
int capacity (void) const { return cap; }
void capacity (int min_cap);
void growTo (int size);
// Stack interface:
void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
- void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
- void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ void push_(const T& elem)
+ {
+ Assert(sz < cap);
+ data[sz++] = elem;
+ }
+ void pop(void)
+ {
+ Assert(sz > 0);
+ sz--, data[sz].~T();
+ }
// NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
// in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
// happen given the way capacities are calculated (below). Essentially, all capacities are
#include "prop/minisat/simp/SimpSolver.h"
+#include "base/check.h"
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
toDimacs();
return l_Undef;
}
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
vec<Var> extra_frozen;
lbool result = l_True;
Var v = var(assumptions[i]);
// If an assumption has been eliminated, remember it.
- assert(!isEliminated(v));
+ Assert(!isEliminated(v));
if (!frozen[v]){
// Freeze and store.
{
#ifndef NDEBUG
if (use_simplification) {
- for (int i = 0; i < ps.size(); i++)
- assert(!isEliminated(var(ps[i])));
+ for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
}
#endif
bool SimpSolver::strengthenClause(CRef cr, Lit l)
{
Clause& c = ca[cr];
- assert(decisionLevel() == 0);
- assert(use_simplification);
+ Assert(decisionLevel() == 0);
+ Assert(use_simplification);
// FIX: this is too inefficient but would be nice to have (properly implemented)
// if (!find(subsumption_queue, &c))
bool SimpSolver::implied(const vec<Lit>& c)
{
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
- trail_lim.push(trail.size());
- for (int i = 0; i < c.size(); i++)
- if (value(c[i]) == l_True){
- cancelUntil(0);
- return false;
- }else if (value(c[i]) != l_False){
- assert(value(c[i]) == l_Undef);
- uncheckedEnqueue(~c[i]);
- }
+ trail_lim.push(trail.size());
+ for (int i = 0; i < c.size(); i++)
+ {
+ if (value(c[i]) == l_True)
+ {
+ cancelUntil(0);
+ return false;
+ }
+ else if (value(c[i]) != l_False)
+ {
+ Assert(value(c[i]) == l_Undef);
+ uncheckedEnqueue(~c[i]);
+ }
+ }
- bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
- cancelUntil(0);
- return result;
+ bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
+ cancelUntil(0);
+ return result;
}
int cnt = 0;
int subsumed = 0;
int deleted_literals = 0;
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
- assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
+ Assert(c.size() > 1
+ || value(c[0]) == l_True); // Unit-clauses should have been
+ // propagated before this point.
// Find best variable to scan:
Var best = var(c[0]);
bool SimpSolver::asymm(Var v, CRef cr)
{
Clause& c = ca[cr];
- assert(decisionLevel() == 0);
+ Assert(decisionLevel() == 0);
if (c.mark() || satisfied(c)) return true;
bool SimpSolver::asymmVar(Var v)
{
- assert(use_simplification);
+ Assert(use_simplification);
- const vec<CRef>& cls = occurs.lookup(v);
+ const vec<CRef>& cls = occurs.lookup(v);
- if (value(v) != l_Undef || cls.size() == 0)
- return true;
+ if (value(v) != l_Undef || cls.size() == 0) return true;
- for (int i = 0; i < cls.size(); i++)
- if (!asymm(v, cls[i]))
- return false;
+ for (int i = 0; i < cls.size(); i++)
+ if (!asymm(v, cls[i])) return false;
- return backwardSubsumptionCheck();
+ return backwardSubsumptionCheck();
}
if (var(c[i]) == v)
v_pos = i + first;
}
- assert(v_pos != -1);
+ Assert(v_pos != -1);
// Swap the first literal with the 'v' literal, so that the literal
// containing 'v' will occur first in the clause:
bool SimpSolver::eliminateVar(Var v)
{
- assert(!frozen[v]);
- assert(!isEliminated(v));
- assert(value(v) == l_Undef);
-
- // Split the occurrences into positive and negative:
- //
- const vec<CRef>& cls = occurs.lookup(v);
- vec<CRef> pos, neg;
- for (int i = 0; i < cls.size(); i++)
- (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
-
- // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
- // clause must exceed the limit on the maximal clause size (if it is set):
- //
- int cnt = 0;
- int clause_size = 0;
+ Assert(!frozen[v]);
+ Assert(!isEliminated(v));
+ Assert(value(v) == l_Undef);
+
+ // Split the occurrences into positive and negative:
+ //
+ const vec<CRef>& cls = occurs.lookup(v);
+ vec<CRef> pos, neg;
+ for (int i = 0; i < cls.size(); i++)
+ (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+ // Check whether the increase in number of clauses stays within the allowed
+ // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
+ // size (if it is set):
+ //
+ int cnt = 0;
+ int clause_size = 0;
+
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+ && (++cnt > cls.size() + grow
+ || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
+ // Delete and store old clauses:
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ eliminated_vars++;
+
+ if (pos.size() > neg.size())
+ {
+ for (int i = 0; i < neg.size(); i++)
+ mkElimClause(elimclauses, v, ca[neg[i]]);
+ mkElimClause(elimclauses, mkLit(v));
+ }
+ else
+ {
for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
- && (++cnt > cls.size() + grow
- || (clause_lim != -1 && clause_size > clause_lim)))
- return true;
-
- // Delete and store old clauses:
- eliminated[v] = true;
- setDecisionVar(v, false);
- eliminated_vars++;
-
- if (pos.size() > neg.size()){
- for (int i = 0; i < neg.size(); i++)
- mkElimClause(elimclauses, v, ca[neg[i]]);
- mkElimClause(elimclauses, mkLit(v));
- }else{
- for (int i = 0; i < pos.size(); i++)
- mkElimClause(elimclauses, v, ca[pos[i]]);
- mkElimClause(elimclauses, ~mkLit(v));
- }
+ mkElimClause(elimclauses, v, ca[pos[i]]);
+ mkElimClause(elimclauses, ~mkLit(v));
+ }
for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
bool SimpSolver::substitute(Var v, Lit x)
{
- assert(!frozen[v]);
- assert(!isEliminated(v));
- assert(value(v) == l_Undef);
+ Assert(!frozen[v]);
+ Assert(!isEliminated(v));
+ Assert(value(v) == l_Undef);
- if (!ok) return false;
+ if (!ok) return false;
- eliminated[v] = true;
- setDecisionVar(v, false);
- const vec<CRef>& cls = occurs.lookup(v);
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ const vec<CRef>& cls = occurs.lookup(v);
- vec<Lit>& subst_clause = add_tmp;
- for (int i = 0; i < cls.size(); i++){
- Clause& c = ca[cls[i]];
+ vec<Lit>& subst_clause = add_tmp;
+ for (int i = 0; i < cls.size(); i++)
+ {
+ Clause& c = ca[cls[i]];
- subst_clause.clear();
- for (int j = 0; j < c.size(); j++){
- Lit p = c[j];
- subst_clause.push(var(p) == v ? x ^ sign(p) : p);
- }
+ subst_clause.clear();
+ for (int j = 0; j < c.size(); j++)
+ {
+ Lit p = c[j];
+ subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+ }
- removeClause(cls[i]);
- ClauseId id = ClauseIdUndef;
- if (!addClause_(subst_clause, c.removable(), id)) {
- return ok = false;
- }
+ removeClause(cls[i]);
+ ClauseId id = ClauseIdUndef;
+ if (!addClause_(subst_clause, c.removable(), id))
+ {
+ return ok = false;
}
+ }
return true;
}
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
- assert(bwdsub_assigns == trail.size());
- assert(subsumption_queue.size() == 0);
- assert(n_touched == 0);
- elim_heap.clear();
- goto cleanup; }
+ Assert(bwdsub_assigns == trail.size());
+ Assert(subsumption_queue.size() == 0);
+ Assert(n_touched == 0);
+ elim_heap.clear();
+ goto cleanup;
+ }
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
checkGarbage(simp_garbage_frac);
}
- assert(subsumption_queue.size() == 0);
+ Assert(subsumption_queue.size() == 0);
}
cleanup:
#ifndef Minisat_SimpSolver_h
#define Minisat_SimpSolver_h
+#include "base/check.h"
#include "cvc4_private.h"
-
#include "proof/clause_id.h"
-#include "prop/minisat/mtl/Queue.h"
#include "prop/minisat/core/Solver.h"
-
+#include "prop/minisat/mtl/Queue.h"
namespace CVC4 {
namespace prop {
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
inline void SimpSolver::updateElimHeap(Var v) {
- assert(use_simplification);
- // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
- if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
- elim_heap.update(v); }
-
+ Assert(use_simplification);
+ // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+ if (elim_heap.inHeap(v)
+ || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+ elim_heap.update(v);
+}
inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
}
}
+int Rational::sgn() const
+{
+ if (cln::zerop(d_value))
+ {
+ return 0;
+ }
+ else if (cln::minusp(d_value))
+ {
+ return -1;
+ }
+ else
+ {
+ Assert(cln::plusp(d_value));
+ return 1;
+ }
+}
+
std::ostream& operator<<(std::ostream& os, const Rational& q){
return os << q.toString();
}
#include <cln/rational_io.h>
#include <cln/real.h>
-#include <cassert>
#include <sstream>
#include <string>
return cln::compare(d_value, x.d_value);
}
- int sgn() const
- {
- if (cln::zerop(d_value))
- {
- return 0;
- }
- else if (cln::minusp(d_value))
- {
- return -1;
- }
- else
- {
- assert(cln::plusp(d_value));
- return 1;
- }
- }
+ int sgn() const;
bool isZero() const { return cln::zerop(d_value); }
** below, in SMT-LIBv2 form (but they're good for all languages).
**/
+#include <cassert>
#include <iostream>
#include <string>
projects / cvc5.git / commitdiff