mirror of
https://github.com/Z3Prover/z3
synced 2025-06-21 13:23:39 +00:00
removed dead files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e2f6a65aa2
commit
181bdb6815
3 changed files with 1 additions and 75 deletions
|
@ -1,34 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2012 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
strategic_solver_cmd.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Specialization of the strategic solver that
|
|
||||||
used cmd_context to access the assertion set.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Leonardo (leonardo) 2012-11-01
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include"strategic_solver_cmd.h"
|
|
||||||
#include"cmd_context.h"
|
|
||||||
|
|
||||||
strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
|
|
||||||
m_ctx(ctx) {
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned strategic_solver_cmd::get_num_assertions() const {
|
|
||||||
return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
|
|
||||||
}
|
|
||||||
|
|
||||||
expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
|
|
||||||
SASSERT(idx < get_num_assertions());
|
|
||||||
return m_ctx.begin_assertions()[idx];
|
|
||||||
}
|
|
|
@ -1,40 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2012 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
strategic_solver_cmd.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Specialization of the strategic solver that
|
|
||||||
used cmd_context to access the assertion set.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Leonardo (leonardo) 2012-11-01
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#ifndef _STRATEGIC_SOLVER_CMD_H_
|
|
||||||
#define _STRATEGIC_SOLVER_CMD_H_
|
|
||||||
|
|
||||||
#include"strategic_solver.h"
|
|
||||||
|
|
||||||
class cmd_context;
|
|
||||||
|
|
||||||
/**
|
|
||||||
Specialization for the SMT 2.0 command language frontend.
|
|
||||||
|
|
||||||
The strategic solver does not have to maintain a copy of the assertion set in the cmd_context.
|
|
||||||
*/
|
|
||||||
class strategic_solver_cmd : public strategic_solver_core {
|
|
||||||
cmd_context & m_ctx;
|
|
||||||
public:
|
|
||||||
strategic_solver_cmd(cmd_context & ctx);
|
|
||||||
virtual unsigned get_num_assertions() const;
|
|
||||||
virtual expr * get_assertion(unsigned idx) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif
|
|
|
@ -18,7 +18,7 @@ Notes:
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
#include"cmd_context.h"
|
#include"cmd_context.h"
|
||||||
#include"strategic_solver_cmd.h"
|
#include"strategic_solver.h"
|
||||||
#include"qfbv_tactic.h"
|
#include"qfbv_tactic.h"
|
||||||
#include"qflia_tactic.h"
|
#include"qflia_tactic.h"
|
||||||
#include"qfnia_tactic.h"
|
#include"qfnia_tactic.h"
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue