Skip to content

Commit

Permalink
👕 refactor: Lint all JavaScript sources.
Browse files Browse the repository at this point in the history
  • Loading branch information
make-github-pseudonymous-again committed Apr 14, 2021
1 parent 8821217 commit 052cc91
Show file tree
Hide file tree
Showing 29 changed files with 461 additions and 475 deletions.
40 changes: 18 additions & 22 deletions doc/scripts/header.js
Original file line number Diff line number Diff line change
@@ -1,34 +1,30 @@
var domReady = function(callback) {
var state = document.readyState ;
if ( state === 'interactive' || state === 'complete' ) {
callback() ;
}
else {
const domReady = function (callback) {
const state = document.readyState;
if (state === 'interactive' || state === 'complete') {
callback();
} else {
document.addEventListener('DOMContentLoaded', callback);
}
} ;

};

domReady(function(){

var projectname = document.createElement('a');
domReady(() => {
const projectname = document.createElement('a');
projectname.classList.add('project-name');
projectname.text = 'aureooms/js-sat';
projectname.href = './index.html' ;
projectname.href = './index.html';

var header = document.getElementsByTagName('header')[0] ;
header.insertBefore(projectname,header.firstChild);
const header = document.querySelectorAll('header')[0];
header.insertBefore(projectname, header.firstChild);

var testlink = document.querySelector('header > a[data-ice="testLink"]') ;
testlink.href = 'https://coveralls.io/github/aureooms/js-sat' ;
testlink.target = '_BLANK' ;
const testlink = document.querySelector('header > a[data-ice="testLink"]');
testlink.href = 'https://coveralls.io/github/aureooms/js-sat';
testlink.target = '_BLANK';

var searchBox = document.querySelector('.search-box');
var input = document.querySelector('.search-input');
const searchBox = document.querySelector('.search-box');
const input = document.querySelector('.search-input');

// active search box when focus on searchBox.
input.addEventListener('focus', function(){
// Active search box when focus on searchBox.
input.addEventListener('focus', () => {
searchBox.classList.add('active');
});

});
9 changes: 3 additions & 6 deletions src/api/decide.js
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
import { solve } from "./solve.js" ;

export function decide ( instance ) {

return !solve( instance ).next( ).done ;
import {solve} from './solve.js';

export function decide(instance) {
return !solve(instance).next().done;
}

17 changes: 11 additions & 6 deletions src/api/from.js
Original file line number Diff line number Diff line change
@@ -1,4 +1,9 @@
import { ParitiesInstance , _sign_to_parity, _keys_to_parity, _parse_DIMACS_CNF } from "../core/index.js" ;
import {
ParitiesInstance,
_sign_to_parity,
_keys_to_parity,
_parse_DIMACS_CNF,
} from '../core/index.js';

/**
* The input is converted to parity format in each case.
Expand All @@ -10,22 +15,22 @@ export const from = {
* variable's label, and a negative literal is represented by the successor
* of the double of its variable's label.
*/
parities : ( clauses ) => new ParitiesInstance( clauses ) ,
parities: (clauses) => new ParitiesInstance(clauses),
/**
* The input is in signs format where variables are given integer labels
* 1 to n, a positive literal is represented by its variable's label, and a
* negative literal is represented by the opposite of its variable's label.
*/
signs : _sign_to_parity ,
signs: _sign_to_parity,
/**
* The input is in keys format where variables are given arbitrary object labels,
* a literal is represented by a pair from the set {true, false} x
* labels, where the first item in the pair is true if the literal is positive,
* and false otherwise.
*/
keys : _keys_to_parity ,
keys: _keys_to_parity,
/**
* Parses a character iterable in DIMACS CNF format.
*/
dcnf : ( iterable ) => new ParitiesInstance( _parse_DIMACS_CNF( iterable ) )
} ;
dcnf: (iterable) => new ParitiesInstance(_parse_DIMACS_CNF(iterable)),
};
8 changes: 4 additions & 4 deletions src/api/index.js
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
export * from "./decide.js" ;
export * from "./from.js" ;
export * from "./solve.js" ;
export * from "./verify.js" ;
export * from './decide.js';
export * from './from.js';
export * from './solve.js';
export * from './verify.js';
10 changes: 4 additions & 6 deletions src/api/solve.js
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
import { SAT0W , setup_watchlist, setup_assignment } from "../core/index.js" ;
import {SAT0W, setup_watchlist, setup_assignment} from '../core/index.js';

/**
* Yields all satisfying assignments for the input instance.
*
* @returns {Iterable} Generator of the satisfying assignments.
*/
export function* solve ( { clauses , n } ) {

yield* SAT0W( n , clauses , setup_watchlist( n , clauses ) , setup_assignment( n ) , 0 ) ;

export function* solve({clauses, n}) {
// eslint-disable-next-line new-cap
yield* SAT0W(n, clauses, setup_watchlist(n, clauses), setup_assignment(n), 0);
}

4 changes: 2 additions & 2 deletions src/api/verify.js
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
import { _verify } from "../core/index.js" ;
export const verify = ( { clauses } , certificate ) => _verify( clauses , certificate ) ;
import {_verify} from '../core/index.js';
export const verify = ({clauses}, certificate) => _verify(clauses, certificate);
49 changes: 23 additions & 26 deletions src/core/SAT0W/SAT0W.js
Original file line number Diff line number Diff line change
@@ -1,27 +1,24 @@
import { update_watchlist } from "./update_watchlist.js" ;

export function* SAT0W ( n , clauses , watchlist , assignment , d ) {

/**
* Recursively solve SAT by assigning to variables d, d+1, ..., n-1. Assumes
* variables 0, ..., d-1 are assigned so far. A generator for all the
* satisfying assignments is returned.
*/
if ( d === n ) {
yield assignment ;
return ;
}

for ( let a of [ 0 , 1 ] ) {

assignment[d] = a ;

if ( update_watchlist( watchlist , (d << 1) | a , assignment ) ) {
yield* SAT0W( n , clauses , watchlist , assignment , d + 1 ) ;
}

}

assignment[d] = -1 ;

import {update_watchlist} from './update_watchlist.js';

export function* SAT0W(n, clauses, watchlist, assignment, d) {
/**
* Recursively solve SAT by assigning to variables d, d+1, ..., n-1. Assumes
* variables 0, ..., d-1 are assigned so far. A generator for all the
* satisfying assignments is returned.
*/
if (d === n) {
yield assignment;
return;
}

for (const a of [0, 1]) {
assignment[d] = a;

if (update_watchlist(watchlist, (d << 1) | a, assignment)) {
// eslint-disable-next-line new-cap
yield* SAT0W(n, clauses, watchlist, assignment, d + 1);
}
}

assignment[d] = -1;
}
6 changes: 3 additions & 3 deletions src/core/SAT0W/index.js
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
export * from "./SAT0W.js" ;
export * from "./setup_watchlist.js" ;
export * from "./update_watchlist.js" ;
export * from './SAT0W.js';
export * from './setup_watchlist.js';
export * from './update_watchlist.js';
18 changes: 8 additions & 10 deletions src/core/SAT0W/setup_watchlist.js
Original file line number Diff line number Diff line change
@@ -1,14 +1,12 @@
export function setup_watchlist ( n , clauses ) {
export function setup_watchlist(n, clauses) {
const watchlist = [];

let watchlist = [ ] ;
for (let i = 0; i < 2 * n; ++i) watchlist.push([]);

for ( let i = 0 ; i < 2 * n ; ++i ) watchlist.push( [ ] ) ;

for ( let clause of clauses ) {
//# Make the clause watch its first literal
watchlist[clause[0]].push( clause ) ;
}

return watchlist ;
for (const clause of clauses) {
// # Make the clause watch its first literal
watchlist[clause[0]].push(clause);
}

return watchlist;
}
61 changes: 28 additions & 33 deletions src/core/SAT0W/update_watchlist.js
Original file line number Diff line number Diff line change
@@ -1,34 +1,29 @@
export function update_watchlist ( watchlist , false_literal , assignment ) {

/**
* Updates the watch list after literal 'false_literal' was just assigned
* False, by making any clause watching false_literal watch something else.
* Returns False it is impossible to do so, meaning a clause is contradicted
* by the current assignment.
*/
while ( watchlist[false_literal].length ) {

let clause = watchlist[false_literal][watchlist[false_literal].length - 1] ;
let found_alternative = false ;

for ( let alternative of clause ) {

let v = alternative >>> 1 ;
let a = alternative & 1 ;

if ( assignment[v] === -1 || assignment[v] === a ^ 1 ) {
found_alternative = true ;
watchlist[false_literal].pop( ) ;
watchlist[alternative].push( clause ) ;
break ;
}

}

if ( !found_alternative ) return false ;

}

return true ;

export function update_watchlist(watchlist, false_literal, assignment) {
/**
* Updates the watch list after literal 'false_literal' was just assigned
* False, by making any clause watching false_literal watch something else.
* Returns False it is impossible to do so, meaning a clause is contradicted
* by the current assignment.
*/
while (watchlist[false_literal].length > 0) {
const clause =
watchlist[false_literal][watchlist[false_literal].length - 1];
let found_alternative = false;

for (const alternative of clause) {
const v = alternative >>> 1;
const a = alternative & 1;

if (assignment[v] === -1 || (assignment[v] === a) ^ 1) {
found_alternative = true;
watchlist[false_literal].pop();
watchlist[alternative].push(clause);
break;
}
}

if (!found_alternative) return false;
}

return true;
}
21 changes: 8 additions & 13 deletions src/core/_verify.js
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

/**
* Verifies that an assignment vector satisfies a k-CNF formula given as a list
* of clauses. The list of clauses and the assignment vector are in parity
Expand All @@ -9,20 +8,16 @@
* @returns {Boolean} Whether the assignment satisfies the k-CNF formula
* represented by the list of clauses.
*/
export function _verify ( clauses , assignment ) {

loop : for ( const clause of clauses ) {

for ( const literal of clause ) {

if ( ( literal ^ assignment[literal >>> 1] ) & 1 ) continue loop ;

export function _verify(clauses, assignment) {
// eslint-disable-next-line no-labels
loop: for (const clause of clauses) {
for (const literal of clause) {
// eslint-disable-next-line no-labels
if ((literal ^ assignment[literal >>> 1]) & 1) continue loop;
}

return false ;

return false;
}

return true ;

return true;
}
16 changes: 7 additions & 9 deletions src/core/convert/KeysInstance.js
Original file line number Diff line number Diff line change
@@ -1,22 +1,20 @@
import { _certificate_to_keys } from "./_certificate_to_keys.js" ;
import {_certificate_to_keys} from './_certificate_to_keys.js';

export class KeysInstance {

/**
* Clauses are in parity format. The variables parameters maps parity
* format literals back to variable names.
*/
constructor ( variables , clauses ) {
this.variables = variables ;
this.clauses = clauses ;
this.n = this.variables.length ;
constructor(variables, clauses) {
this.variables = variables;
this.clauses = clauses;
this.n = this.variables.length;
}

/**
* Returns an object that maps each variable name to a variable assignment.
*/
assignment ( certificate ) {
return _certificate_to_keys( this.variables , certificate ) ;
assignment(certificate) {
return _certificate_to_keys(this.variables, certificate);
}

}
14 changes: 6 additions & 8 deletions src/core/convert/ParitiesInstance.js
Original file line number Diff line number Diff line change
@@ -1,20 +1,18 @@
import { _count } from "./_count.js" ;
import {_count} from './_count.js';

export class ParitiesInstance {

/**
* Clauses are in parity format.
*/
constructor ( clauses ) {
this.clauses = clauses ;
this.n = _count( clauses ) ;
constructor(clauses) {
this.clauses = clauses;
this.n = _count(clauses);
}

/**
* Returns assignment vector in parity format.
*/
assignment ( certificate ) {
return certificate.slice( ) ;
assignment(certificate) {
return certificate.slice();
}

}
14 changes: 6 additions & 8 deletions src/core/convert/SignsInstance.js
Original file line number Diff line number Diff line change
@@ -1,20 +1,18 @@
import { _count } from "./_count.js" ;
import {_count} from './_count.js';

export class SignsInstance {

/**
* Clauses are in parity format.
*/
constructor ( clauses ) {
this.clauses = clauses ;
this.n = _count( clauses ) ;
constructor(clauses) {
this.clauses = clauses;
this.n = _count(clauses);
}

/**
* Returns assignment vector in signs format.
*/
assignment ( certificate ) {
return [ 0 ].concat( certificate ) ;
assignment(certificate) {
return [0].concat(certificate);
}

}
Loading

0 comments on commit 052cc91

Please sign in to comment.