luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-09-03 08:25:20 +02:00
Code Issues Packages Projects Releases Wiki Activity

Version abc81004

Browse Source
This commit is contained in:
Alan Mishchenko
2008-10-04 08:01:00 -07:00
parent 689cbe904e
commit eb75697fe0
39 changed files with 10033 additions and 139 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/sat/bsat/satChecker.c
+187
View File
@@ -0,0 +1,187 @@
/**CFile****************************************************************
FileName [satChecker.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sat_solver.]
Synopsis [Resolution proof checker.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: satChecker.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_PrintClause( Vec_Vec_t * vClauses, int Clause )
{
Vec_Int_t * vClause;
int i, Entry;
printf( "Clause %d: {", Clause );
vClause = Vec_VecEntry( vClauses, Clause );
Vec_IntForEachEntry( vClause, Entry, i )
printf( " %d", Entry );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sat_ProofResolve( Vec_Vec_t * vClauses, int Result, int Clause1, int Clause2 )
{
Vec_Int_t * vResult = Vec_VecEntry( vClauses, Result );
Vec_Int_t * vClause1 = Vec_VecEntry( vClauses, Clause1 );
Vec_Int_t * vClause2 = Vec_VecEntry( vClauses, Clause2 );
int Entry1, Entry2, ResVar;
int i, j, Counter = 0;
Vec_IntForEachEntry( vClause1, Entry1, i )
Vec_IntForEachEntry( vClause2, Entry2, j )
if ( Entry1 == -Entry2 )
{
ResVar = Entry1;
Counter++;
}
if ( Counter != 1 )
{
printf( "Error: Clause %d = Resolve(%d, %d): The number of pivot vars is %d.\n",
Result, Clause1, Clause2, Counter );
Sat_PrintClause( vClauses, Clause1 );
Sat_PrintClause( vClauses, Clause2 );
return 0;
}
// create new clause
assert( Vec_IntSize(vResult) == 0 );
Vec_IntForEachEntry( vClause1, Entry1, i )
if ( Entry1 != ResVar && Entry1 != -ResVar )
Vec_IntPushUnique( vResult, Entry1 );
assert( Vec_IntSize(vResult) + 1 == Vec_IntSize(vClause1) );
Vec_IntForEachEntry( vClause2, Entry2, i )
if ( Entry2 != ResVar && Entry2 != -ResVar )
Vec_IntPushUnique( vResult, Entry2 );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofChecker( char * pFileName )
{
FILE * pFile;
Vec_Vec_t * vClauses;
int c, i, Num, RetValue, Counter, Counter2, Clause1, Clause2;
// open the file
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
return;
// count the number of clauses
Counter = Counter2 = 0;
while ( (c = fgetc(pFile)) != EOF )
{
Counter += (c == '\n');
Counter2 += (c == '*');
}
vClauses = Vec_VecStart( Counter+1 );
printf( "The proof contains %d roots and %d resolution steps.\n", Counter-Counter2, Counter2 );
// read the clauses
rewind( pFile );
for ( i = 1 ; ; i++ )
{
RetValue = fscanf( pFile, "%d", &Num );
if ( RetValue != 1 )
break;
assert( Num == i );
while ( (c = fgetc( pFile )) == ' ' );
if ( c == '*' )
{
RetValue = fscanf( pFile, "%d %d", &Clause1, &Clause2 );
assert( RetValue == 2 );
RetValue = fscanf( pFile, "%d", &Num );
assert( RetValue == 1 );
assert( Num == 0 );
if ( !Sat_ProofResolve( vClauses, i, Clause1, Clause2 ) )
{
printf( "Error detected in the resolution proof.\n" );
Vec_VecFree( vClauses );
fclose( pFile );
return;
}
}
else
{
ungetc( c, pFile );
while ( 1 )
{
RetValue = fscanf( pFile, "%d", &Num );
assert( RetValue == 1 );
if ( Num == 0 )
break;
Vec_VecPush( vClauses, i, (void *)Num );
}
RetValue = fscanf( pFile, "%d", &Num );
assert( RetValue == 1 );
assert( Num == 0 );
}
}
assert( i-1 == Counter );
if ( Vec_IntSize( Vec_VecEntry(vClauses, Counter) ) != 0 )
printf( "The last clause is not empty.\n" );
else
printf( "The empty clause is derived.\n" );
Vec_VecFree( vClauses );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/bsat/satInterA.c
+26
View File
@@ -701,6 +701,10 @@ p->timeTrace += clock() - clk;
// Inta_ManPrintInterOne( p, pFinal );
}
Inta_ManProofSet( p, pFinal, p->Counter );
// make sure the same proof ID is not asssigned to two consecutive clauses
assert( p->pProofNums[pFinal->Id-1] != p->Counter );
// if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] )
// p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id];
return p->Counter;
}
@@ -748,6 +752,27 @@ int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
{
assert( 0 ); // cannot prove
return 0;
}
// skip the clause if it is weaker or the same as the conflict clause
if ( pClause->nLits >= pConflict->nLits )
{
// check if every literal of conflict clause can be found in the given clause
int j;
for ( i = 0; i < (int)pConflict->nLits; i++ )
{
for ( j = 0; j < (int)pClause->nLits; j++ )
if ( pConflict->pLits[i] == pClause->pLits[j] )
break;
if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
break;
}
if ( i == (int)pConflict->nLits ) // all lits are found
{
// undo to the root level
Inta_ManCancelUntil( p, p->nRootSize );
return 1;
}
}
// construct the proof
@@ -973,6 +998,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( p->fProofWrite )
{
fclose( p->pFile );
// Sat_ProofChecker( "proof.cnf_" );
p->pFile = NULL;
}
src/sat/bsat/satInterA_mod.c
+1104
View File
File diff suppressed because it is too large Load Diff
src/sat/bsat/satInterA_old.c
+1047
View File
File diff suppressed because it is too large Load Diff
src/sat/bsat/satInterA_yu_hu.c
+60 -27
View File
@@ -114,6 +114,7 @@ Inta_Man_t * Inta_ManAlloc()
// parameters
p->fProofWrite = 1;
p->fProofVerif = 1;
return p;
}
@@ -289,16 +290,6 @@ void Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause )
printf( " }\n" );
}
// Yu Hu
void Inta_ManPrintClauseEx( lit * pResLits, int nResLits )
{
int i;
printf( " {" );
for ( i = 0; i < nResLits; i++ )
printf( " %d", lit_print(pResLits[i]) );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Prints the resolvent.]
@@ -315,6 +306,8 @@ void Inta_ManPrintResolvent( lit * pResLits, int nResLits )
int i;
printf( "Resolvent: {" );
for ( i = 0; i < nResLits; i++ )
// Yu Hu
// printf( " %d", pResLits[i] );
printf( " %d", lit_print(pResLits[i]) );
printf( " }\n" );
}
@@ -537,6 +530,17 @@ void Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause )
}
}
// Yu Hu
void Inta_ManPrintClauseEx( lit * pResLits, int nResLits )
{
int i;
printf( " {" );
for ( i = 0; i < nResLits; i++ )
printf( " %d", lit_print(pResLits[i]) );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Traces the proof for one clause.]
@@ -594,7 +598,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
for ( v = 1; v < (int)pReason->nLits; v++ )
p->pSeens[lit_var(pReason->pLits[v])] = 1;
// record the reason clause
assert( Inta_ManProofGet(p, pReason) > 0 );
p->Counter++;
@@ -617,14 +620,15 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
if ( p->fProofVerif )
{
int v1, v2;
// Yu Hu
// if ( fPrint )
// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
if ( fPrint ) {
printf("pivot = %d,\n", lit_print(p->pTrail[i]));
Inta_ManPrintClauseEx( p->pResLits, p->nResLits);
}
// if ( fPrint )
// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
if ( fPrint ) {
printf("pivot = %d,\n", lit_print(p->pTrail[i]));
Inta_ManPrintClauseEx( p->pResLits, p->nResLits);
}
// check that the var is present in the resolvent
for ( v1 = 0; v1 < p->nResLits; v1++ )
if ( lit_var(p->pResLits[v1]) == Var )
@@ -660,12 +664,12 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
}
// Yu Hu
if ( fPrint ) {
Inta_ManPrintClauseEx( pReason->pLits, pReason->nLits);
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
}
}
if ( fPrint ) {
Inta_ManPrintClauseEx( pReason->pLits, pReason->nLits);
Inta_ManPrintResolvent( p->pResLits, p->nResLits);
}
}
// Vec_PtrPush( pFinal->pAntis, pReason );
}
@@ -680,10 +684,11 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
if ( p->fProofVerif )
{
int v1, v2;
if ( fPrint ){
// Yu Hu
// Yu Hu
// if ( fPrint )
// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
}
for ( v1 = 0; v1 < p->nResLits; v1++ )
{
for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
@@ -700,6 +705,27 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
// if there are literals in the clause that are not in the resolvent
// it means that the derived resolvent is stronger than the clause
// we can replace the clause with the resolvent by removing these literals
if ( p->nResLits != (int)pFinal->nLits )
{
for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
{
for ( v2 = 0; v2 < p->nResLits; v2++ )
if ( pFinal->pLits[v1] == p->pResLits[v2] )
break;
if ( v2 < p->nResLits )
continue;
// remove literal v1 from the final clause
pFinal->nLits--;
for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
pFinal->pLits[v2] = pFinal->pLits[v2+1];
v1--;
}
assert( p->nResLits == (int)pFinal->nLits );
}
}
p->timeTrace += clock() - clk;
@@ -733,9 +759,16 @@ int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
if ( pClause->nLits == 0 )
printf( "Error: Empty clause is attempted.\n" );
// add assumptions to the trail
assert( !pClause->fRoot );
assert( p->nTrailSize == p->nRootSize );
// if any of the clause literals are already assumed
// it means that the clause is redundant and can be skipped
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
return 1;
// add assumptions to the trail
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{
src/sat/lsat/solver.h
+124
View File
@@ -0,0 +1,124 @@
/****************************************************************************************[solver.h]
Copyright (c) 2008, Niklas Sorensson
2008, Koen Claessen
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#ifndef Minisat_solver_h
#define Minisat_solver_h
// SolverTypes:
//
typedef struct solver_t solver;
typedef int solver_Var;
typedef int solver_Lit;
typedef int solver_lbool;
// Constants: (can these be made inline-able?)
//
extern const solver_lbool solver_l_True;
extern const solver_lbool solver_l_False;
extern const solver_lbool solver_l_Undef;
solver* solver_new (void);
void solver_delete (solver* s);
solver_Var solver_newVar (solver *s);
solver_Lit solver_newLit (solver *s);
solver_Lit solver_mkLit (solver_Var x);
solver_Lit solver_mkLit_args (solver_Var x, int sign);
solver_Lit solver_negate (solver_Lit p);
solver_Var solver_var (solver_Lit p);
int solver_sign (solver_Lit p);
int solver_addClause (solver *s, int len, solver_Lit *ps);
void solver_addClause_begin (solver *s);
void solver_addClause_addLit(solver *s, solver_Lit p);
int solver_addClause_commit(solver *s);
int solver_simplify (solver *s);
int solver_solve (solver *s, int len, solver_Lit *ps);
void solver_solve_begin (solver *s);
void solver_solve_addLit (solver *s, solver_Lit p);
int solver_solve_commit (solver *s);
int solver_okay (solver *s);
void solver_setPolarity (solver *s, solver_Var v, int b);
void solver_setDecisionVar (solver *s, solver_Var v, int b);
solver_lbool solver_get_l_True (void);
solver_lbool solver_get_l_False (void);
solver_lbool solver_get_l_Undef (void);
solver_lbool solver_value_Var (solver *s, solver_Var x);
solver_lbool solver_value_Lit (solver *s, solver_Lit p);
solver_lbool solver_modelValue_Var (solver *s, solver_Var x);
solver_lbool solver_modelValue_Lit (solver *s, solver_Lit p);
int solver_num_assigns (solver *s);
int solver_num_clauses (solver *s);
int solver_num_learnts (solver *s);
int solver_num_vars (solver *s);
int solver_num_freeVars (solver *s);
int solver_conflict_len (solver *s);
solver_Lit solver_conflict_nthLit (solver *s, int i);
// Setters:
void solver_set_verbosity (solver *s, int v);
// Getters:
int solver_num_conflicts (solver *s);
/* TODO
// Mode of operation:
//
int verbosity;
double var_decay;
double clause_decay;
double random_var_freq;
double random_seed;
double restart_luby_start; // The factor with which the values of the luby sequence is multiplied to get the restart (default 100)
double restart_luby_inc; // The constant that the luby sequence uses powers of (default 2)
bool expensive_ccmin; // FIXME: describe.
bool rnd_pol; // FIXME: describe.
int restart_first; // The initial restart limit. (default 100)
double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
int learntsize_adjust_start_confl;
double learntsize_adjust_inc;
// Statistics: (read-only member variable)
//
uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
*/
#endif